Documentation

Lean.Elab.Tactic.Rfl

rfl tactic extension for reflexive relations #

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

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