Lean.Meta.Inductive

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

Equations

Lean.Meta.compatibleCtors ctorName₁ ctorName₂ = do let ctorInfo₁ ← Lean.getConstInfoCtor ctorName₁ let ctorInfo₂ ← Lean.getConstInfoCtor ctorName₂ if (ctorInfo₁.induct != ctorInfo₂.induct) = true then pure false else do let discr ← Lean.Meta.forallMetaTelescope ctorInfo₁.toConstantVal.type Lean.MetavarKind.natural let x : Array Lean.Expr × Array Lean.BinderInfo × Lean.Expr := discr match x with | (x, x_1, ctorType₁) => do let discr ← Lean.Meta.forallMetaTelescope ctorInfo₂.toConstantVal.type Lean.MetavarKind.natural let x : Array Lean.Expr × Array Lean.BinderInfo × Lean.Expr := discr match x with | (x, x_2, ctorType₂) => Lean.Meta.isDefEq ctorType₁ ctorType₂