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

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

Equations

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

def Duper.mkDatatypeInjectivityPosProof (removedLitNum ctorArgNum : 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.mkDatatypeInjectivityNegProof (removedLitNum : 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.datatypeInjectivity : MSimpRule

Implements the injectivity rules described in section 6.3 of https://arxiv.org/pdf/1611.02908

Equations

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