Documentation

Mathlib.Lean.Meta

Additional utilities in Lean.MVarId #

Replace hypothesis hyp in goal g with proof : typeNew. The new hypothesis is given the same user name as the original, it attempts to avoid reordering hypotheses, and the original is cleared if possible.

Equations
  • One or more equations did not get rendered due to their size.

Finds the LocalDecl for the FVar in e with the highest index.

Equations
  • One or more equations did not get rendered due to their size.

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

Equations

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

Equations
  • One or more equations did not get rendered due to their size.

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

Return local hypotheses which are not "implementation detail", as Exprs.

Equations
  • One or more equations did not get rendered due to their size.

Given a monadic function F that takes a type and a term of that type and produces a new term, lifts this to the monadic function that opens a telescope, applies F to the body, and then builds the lambda telescope term for the new term.

Equations
  • One or more equations did not get rendered due to their size.

Given a monadic function F that takes a term and produces a new term, lifts this to the monadic function that opens a telescope, applies F to the body, and then builds the lambda telescope term for the new term.

Equations

Analogue of liftMetaTactic for tactics that return a single goal.

Equations

Analogue of liftMetaTactic for tactics that do not return any goals.

Equations

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

Equations
  • One or more equations did not get rendered due to their size.