Def Mathlib.Tactic.Hint.getHints

Modification history

2025-08-19 02:31
Mathlib/Tactic/Hint.lean
feat: add priority to hint tactics (#28509) …
Modified Mathlib.Tactic.Hint.getHintsView on Github →
2023-11-16 01:34
Mathlib/Tactic/Hint.lean
feat: the 'hint' tactic (#8363) …
Added Mathlib.Tactic.Hint.getHintsView on Github →