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
- Lean.MVarId.note g h v t = do let __do_lift ← Option.getDM t (Lean.Meta.inferType v) let __do_lift ← Lean.MVarId.assert g h __do_lift v Lean.MVarId.intro1P __do_lift
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
- Lean.MVarId.intros! mvarId = Lean.MVarId.intros!.run mvarId #[] mvarId
Implementation of intros!
.
Return local hypotheses which are not "implementation detail", as Expr
s.
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
- Lean.Meta.mapForallTelescope F forallTerm = Lean.Meta.mapForallTelescope' (fun x e => F e) forallTerm
Analogue of liftMetaTactic
for tactics that return a single goal.
Equations
- Lean.Elab.Tactic.liftMetaTactic' tac = Lean.Elab.Tactic.liftMetaTactic fun g => do let __do_lift ← tac g pure [__do_lift]
Analogue of liftMetaTactic
for tactics that do not return any goals.
Equations
- Lean.Elab.Tactic.liftMetaFinishingTactic tac = Lean.Elab.Tactic.liftMetaTactic fun g => do tac g pure []
Copy of Lean.Elab.Tactic.run
that can return a value.
Equations
- One or more equations did not get rendered due to their size.