Extending have, let and suffices

This file extends the have, let and suffices tactics to allow the addition of hypotheses to the context without requiring their proofs to be provided immediately.

def Mathlib.Tactic.optBinderIdent : Lean.Parser.Parser

A parser for optional binder identifiers

Equations

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

def Mathlib.Tactic.optBinderIdent.name (id : Lean.TSyntax `Mathlib.Tactic.optBinderIdent) : Lean.Name

Retrieves the name of the optional identifier, if provided. Returns this otherwise

Equations

• Mathlib.Tactic.optBinderIdent.name id = if Lean.Syntax.isIdent id.raw[0] = true then Lean.Syntax.getId id.raw[0] else Lean.TSyntax.getId (Lean.HygieneInfo.mkIdent { raw := id.raw[0] } `this)

def Mathlib.Tactic.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.

def Mathlib.Tactic.tacticHave_ : Lean.ParserDescr

Equations

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

def Mathlib.Tactic.tacticLet_ : Lean.ParserDescr

Equations

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

def Mathlib.Tactic.tacticSuffices_ : Lean.ParserDescr

Equations

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

def Mathlib.Tactic.haveLetCore (goal : Lean.MVarId) (name : Lean.TSyntax `Mathlib.Tactic.optBinderIdent) (bis : Array (Lean.TSyntax `Lean.Parser.Term.letIdBinder)) (t : Option Lean.Term) (keepTerm : Bool) : Lean.Elab.TermElabM (Lean.MVarId × Lean.MVarId)

Adds hypotheses to the context, turning them into goals to be proved later if their proof terms aren't provided (t: Option Term := none).

If the bound term is intended to be kept in the context, pass keepTerm : Bool := true. This is useful when extending the let tactic, which is expected to show the proof term in the infoview.

Equations

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