ink

def Lean.Parser.Term.haveIdLhs' : Lean.Parser.Parser

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.

ink

def Mathlib.Tactic.tacticHave_ : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Mathlib.Tactic.tacticLet_ : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Mathlib.Tactic.tacticSuffices_ : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Mathlib.Tactic.haveLetCore (goal : Lean.MVarId) (name : Option Lean.Syntax) (bis : Array Lean.Syntax) (t : Option Lean.Syntax) (keepTerm : Bool) : Lean.Elab.TermElabM (Lean.MVarId × Lean.MVarId)

Equations

• One or more equations did not get rendered due to their size.