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.

A parser for optional binder identifiers

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    def Mathlib.Tactic.optBinderIdent.name (id : Lean.TSyntax `Mathlib.Tactic.optBinderIdent) :

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

    Equations
    Instances For

      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
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              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) :

              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