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

def Std.Tactic.reflExt.config : Lean.Meta.WhnfCoreConfig

Discrimation tree settings for the refl extension.

Equations

• Std.Tactic.reflExt.config = { iota := true, beta := true, proj := Lean.Meta.ProjReductionKind.yesWithDelta, zeta := true }

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

Environment extensions for refl lemmas

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, a relation which has a reflexive lemma tagged with the attribute [refl].

Equations

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