Try to synthesize instances for the metavariables mvars
.
Returns metavariables that still need to be synthesized.
We can view the resulting array as the set of metavariables that we should try again.
This is needed when applying or rewriting with functions with complex instances.
For example, consider rw [@map_smul]
where map_smul
is
map_smul {F : Type u_1} {M : Type u_2} {N : Type u_3} {φ : M → N}
{X : Type u_4} {Y : Type u_5}
[SMul M X] [SMul N Y] [FunLike F X Y] [MulActionSemiHomClass F φ X Y]
(f : F) (c : M) (x : X) : DFunLike.coe f (c • x) = φ c • DFunLike.coe f x
and MulActionSemiHomClass
is defined as
class MulActionSemiHomClass (F : Type _)
{M N : outParam (Type _)} (φ : outParam (M → N))
(X Y : outParam (Type _)) [SMul M X] [SMul N Y] [FunLike F X Y] : Prop where
The left-hand-side of the equation does not bind N
. Thus, SMul N Y
cannot
be synthesized until we synthesize MulActionSemiHomClass F φ X Y
. Note that
N
is an output parameter for MulActionSemiHomClass
.
Equations
Instances For
Equations
Instances For
If synthAssignedInstances
is true
, then apply
will synthesize instance implicit arguments
even if they have assigned by isDefEq
, and then check whether the synthesized value matches the
one inferred. The congr
tactic sets this flag to false.
Equations
Instances For
Close the given goal using apply e
.
Equations
Instances For
Equations
Instances For
Short-hand for applying a constant to the goal.
Equations
Instances For
Try to convert an Iff
into an Eq
by applying iff_of_eq
.
If successful, returns the new goal, and otherwise returns the original MVarId
.
This may be regarded as being a special case of Lean.MVarId.liftReflToEq
, specifically for Iff
.
Equations
Instances For
Try to close the goal 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
.
Equations
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
.