Documentation

Mathlib.Lean.Meta

Additional utilities in Lean.MVarId #

def Lean.MVarId.let (g : MVarId) (h : Name) (v : Expr) (t : Option Expr := none) :

Add the hypothesis h : t, given v : t, and return the new FVarId.

Equations
    Instances For

      Has the effect of refine ⟨e₁,e₂,⋯, ?_⟩.

      Equations
        Instances For

          Applies intro repeatedly until it fails. We use this instead of Lean.MVarId.intros to allowing unfolding. For example, if we want to do introductions for propositions like ¬p, the ¬ needs to be unfolded into False, and intros does not do such unfolding.

          Equations
            Instances For
              partial def Lean.MVarId.intros!.run (mvarId : MVarId) (acc : Array FVarId) (g : MVarId) :

              Implementation of intros!.

              Get the type the given metavariable after instantiating metavariables and cleaning up annotations.

              Equations
                Instances For

                  Analogue of liftMetaTactic for tactics that return a single goal.

                  Equations
                    Instances For

                      Copy of Lean.Elab.Tactic.run that can return a value.

                      Equations
                        Instances For