# `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]`.

source
opaque Lean.Meta.Rfl.reflExt :
SimpleScopedEnvExtension (Name × Array DiscrTree.Key) (DiscrTree Name)

Environment extensions for `refl` lemmas

source
def Lean.MVarId.applyRfl (goal : MVarId) :
MetaM Unit

`MetaM` version of the `rfl` tactic.

This tactic applies to a goal whose target has the form `x ~ x`, where `~` is a reflexive relation, that is, equality or another relation which has a reflexive lemma tagged with the attribute [refl].

Equations

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

Instances For

source
def Lean.MVarId.liftReflToEq (mvarId : MVarId) :
MetaM 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.

Instances For