Documentation

Mathlib.Lean.Meta

Additional utilities in Lean.MVarId #

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

Equations
  • g.let h v t = do let __do_liftt.getDM (Lean.Meta.inferType v) let __do_liftg.define h __do_lift v __do_lift.intro1P
Instances For

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

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

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

        Equations
        • mvarId.getType'' = do let __do_liftmvarId.getType let __do_liftLean.instantiateMVars __do_lift pure __do_lift.cleanupAnnotations
        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
            • One or more equations did not get rendered due to their size.
            Instances For