diff --git a/doc/hints.md b/doc/hints.md index f980695..591edb1 100644 --- a/doc/hints.md +++ b/doc/hints.md @@ -10,6 +10,8 @@ Statement .... := by ... ``` +Note that hints are only **context-aware but not history-aware**. In particular they only look at the assumptions and the current goal. Player's might encounter hints in a different order - or not at all - if they decide to go for a unique proof idea. The `Branch` tactic helps placing hints outside the sample solution's proof. + ## 1. When do hints show? A hint will be displayed if the player's goal matches the one where the hint was placed in the