Lean.MVarId.liftReflToEq
#
Convert a goal of the form x ~ y
into the form x = y
, where ~
is a reflexive
relation, that is, a relation which has a reflexive lemma tagged with the attribute [refl]
.
If this can't be done, returns the original MVarId
.
This tactic applies to a goal whose target has the form x ~ x
, where ~
is a reflexive
relation, that is, a relation which has a reflexive lemma tagged with the attribute [refl].
Equations
Instances For
Convert a goal of the form x ~ y
into the form x = y
, where ~
is a reflexive
relation, that is, a relation which has a reflexive lemma tagged with the attribute [refl]
.
If this can't be done, returns the original MVarId
.
Equations
- One or more equations did not get rendered due to their size.