def Duper.litComparesDistinctConstructors (lit : Lit) : Lean.MetaM (Option Bool)

Returns none if lit does not compare distinct constructors, returns some false if lit says two distinct constructors are equal, and returns some true if lit says two distinct constructors are not equal.

Equations

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

def Duper.mkDatatypeDistinctnessProof (refs : List (Option Nat)) (premises : List Lean.Expr) (parents : List RuleM.ProofParent) (transferExprs : Array Lean.Expr) (c : Clause) : Lean.MetaM Lean.Expr

Equations

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

def Duper.datatypeDistinctness : MSimpRule

Implements the Dist-S⁺ and Dist-S⁻ rules described in https://arxiv.org/pdf/1611.02908

Equations

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