Def Mathlib.Tactic.Hint.addHint

Modification history

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