class HasAlphaEquiv (β : Type u) : Type u

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

• AlphaEquiv : β → β → Prop

  α-equivalence relation for type β.

def «term_=α_» : Lean.TrailingParserDescr

Equations

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