Documentation

Lean.Meta.Tactic.Rfl

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 :
Lean.SimpleScopedEnvExtension (Lean.Name × Array Lean.Meta.DiscrTree.Key) (Lean.Meta.DiscrTree Lean.Name)

Environment extensions for refl lemmas

source
def Lean.MVarId.applyRfl (goal : Lean.MVarId) :
Lean.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 : 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.
    Instances For