Helper methods for inductive datatypes

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

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

Equations

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