class Cslib.HasAlphaEquiv (β : Type u) : Type u

Typeclass for the α-equivalence notation x =α y.

• AlphaEquiv : β → β → Prop

  α-equivalence relation for type β.

def Cslib.«term_=α_» : Lean.TrailingParserDescr

α-equivalence relation for type β.

Equations

• Cslib.«term_=α_» = Lean.ParserDescr.trailingNode `Cslib.«term_=α_» 1022 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " =α ") (Lean.ParserDescr.cat `term 1024))