Documentation

Mathlib.Tactic.Have

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.

source
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.
Instances For
    source
    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
    Instances For
      source
      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.
      Instances For
        source
        def Mathlib.Tactic.tacticHave_ :
        Lean.ParserDescr
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Mathlib.Tactic.tacticLet_ :
          Lean.ParserDescr
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Mathlib.Tactic.tacticSuffices_ :
            Lean.ParserDescr
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              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.
              Instances For