Def Mathlib.Tactic.Tauto.finishingConstructorMatcher

Modification history

2023-06-29 11:49

Mathlib/Tactic/Tauto.lean

fix: have `tauto` use `Lean.Meta.isProp` rather than `Lean.Expr.isProp` (#5565) …

Modified Mathlib.Tactic.Tauto.finishingConstructorMatcher View on Github →

2022-12-21 04:17

Mathlib/Tactic/Tauto.lean

feat: implement basic version of tauto tactic (#1081) …

Added Mathlib.Tactic.Tauto.finishingConstructorMatcher View on Github →