Additional utilities in Lean.MVarId
#
Solve a goal by synthesizing an instance.
Instances For
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.
Instances For
Finds the LocalDecl
for the FVar in e
with the highest index.
Instances For
Add the hypothesis h : t
, given v : t
, and return the new FVarId
.
Instances For
Add the hypothesis h : t
, given v : t
, and return the new FVarId
.
Instances For
Short-hand for applying a constant to the goal.
Instances For
Has the effect of refine ⟨e₁,e₂,⋯, ?_⟩
.
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.
Instances For
Implementation of intros!
.
Check if a goal is of a subsingleton type.
Instances For
Check if a goal is "independent" of a list of other goals. We say a goal is independent of other goals if assigning a value to it can not change the solvability of the other goals.
This function only calculates a conservative approximation of this condition.
Instances For
Try to close the goal with using proof_irrel_heq
. Returns whether or not it succeeds.
We need to be somewhat careful not to assign metavariables while doing this, otherwise we might
specialize Sort _
to Prop
.
Instances For
Try to close the goal using Subsingleton.elim
. Returns whether or not it succeeds.
We are careful to apply Subsingleton.elim
in a way that does not assign any metavariables.
This is to prevent the Subsingleton Prop
instance from being used as justification to specialize
Sort _
to Prop
.
Instances For
Return local hypotheses which are not "implementation detail", as Expr
s.
Instances For
Count how many local hypotheses appear in an expression.
Instances For
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.
Instances For
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.
Instances For
Get the type the given metavariable after instantiating metavariables and cleaning up annotations.
Instances For
Analogue of liftMetaTactic
for tactics that return a single goal.
Instances For
Analogue of liftMetaTactic
for tactics that do not return any goals.
Instances For
Copy of Lean.Elab.Tactic.run
that can return a value.