rfl tactic extension for reflexive relations

This extends the rfl tactic so that it works on any reflexive relation, provided the reflexivity lemma has been marked as @[refl].

opaque Mathlib.Tactic.reflExt : Lean.SimpleScopedEnvExtension (Lean.Name × Array (Lean.Meta.DiscrTree.Key true)) (Lean.Meta.DiscrTree Lean.Name true)

Environment extensions for refl lemmas

def Lean.MVarId.rfl (goal : Lean.MVarId) : Lean.MetaM Unit

Closes the goal if the 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]. Otherwise throws an error.

See also Lean.MVarId.refl, which is for x = x specifically.

This is the MetaM implementation of the rfl tactic.

Equations

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

def Lean.MVarId.liftReflToEq (mvarId : Lean.MVarId) : Lean.MetaM Lean.MVarId

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.