Uses checkColGt
to prevent
have h
exact Nat
From being interpreted as
have h
exact Nat
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
def
Mathlib.Tactic.haveLetCore
(goal : Lean.MVarId)
(name : Option Lean.Syntax)
(bis : Array Lean.Syntax)
(t : Option Lean.Syntax)
(keepTerm : Bool)
:
Equations
- One or more equations did not get rendered due to their size.