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

.

Environment extensions for `refl`

lemmas

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.

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

.