Def Mathlib.Tactic.elabCheckTactic

Modification history

2026-03-21 09:03
Mathlib/Tactic/Check.lean
feat: add `#check'` command and tactic, which only show explicit arguments (#31194) …
Deleted Mathlib.Tactic.elabCheckTacticView on Github →
2024-02-20 06:59
Mathlib/Tactic/Check.lean
feat: `#check` tactic (#9902) …
Added Mathlib.Tactic.elabCheckTacticView on Github →