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.

As a style choice, this should not be used in mathlib; but is provided for downstream users who preferred the old style.

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

A parser for optional binder identifiers

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

def Mathlib.Tactic.haveIdLhs' : Lean.Parser.Parser

Uses checkColGt to prevent

have h
exact Nat

From being interpreted as

have h
  exact Nat

def Mathlib.Tactic.tacticHave_ : Lean.ParserDescr

def Mathlib.Tactic.tacticLet_ : Lean.ParserDescr

def Mathlib.Tactic.tacticSuffices_ : Lean.ParserDescr

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.