Def Mathlib.Tactic.Hint.hint

Modification history

2025-02-19 15:53

Mathlib/Tactic/Hint.lean

fix: add missing withMainContext for hint (#22077) …

Modified Mathlib.Tactic.Hint.hint View on Github →

2023-11-16 01:34

Mathlib/Tactic/Hint.lean

feat: the 'hint' tactic (#8363) …

Added Mathlib.Tactic.Hint.hint View on Github →