HepLean Documentation

Lean.Meta.Inductive

Helper methods for inductive datatypes #

def Lean.Meta.compatibleCtors (ctorName₁ ctorName₂ : Lean.Name) :

Return true if the types of the given constructors are compatible.

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