Commit 2023-11-16 01:34 5c598152
View on Github →feat: the 'hint' tactic (#8363)
example (h : 1 < 0) : False := by hint
example {P Q : Prop} (p : P) (f : P → Q) : Q := by hint
example {P Q R: Prop} (x : P ∧ Q ∧ R ∧ R) : Q ∧ P ∧ R := by hint
example {a b : ℚ} (h : a < b) : ¬ b < a := by hint
example : 37^2 - 35^2 = 72 * 2 := by hint
example : Nat.Prime 37 := by hint
Tries out any tactics registered using register_hint tac, and reports which ones succeed using the new "Try these: " multiple suggestion widgets. Tactics that close the goal are highlighted in green. Tactics that succeed but don't close the goal display the new subgoals in the widget. If tac produces a "Try this: " message, use that instead of tac.
I haven't hooked up aesop yet, because of https://github.com/leanprover-community/aesop/issues/85. Similarly for norm_num.
I would like to parallelize this, but I don't think that needs to happen right away.