partial def Duper.collectConstructorSubterms (e : Lean.Expr) : Lean.MetaM (Array Lean.Expr)

Produces a list of (possibly duplicate) constructor subterms for e

def Duper.litComparesConstructorSubterms (lit : Lit) : Lean.MetaM (Option LitSide)

Returns none if lit does not compare constructor subterms, and returns some litside if lit.litside is a subterm of the constructor it is being compared to. Note that lit.litside may not itself be a constructor (e.g. xs is a constructor subterm of x :: xs)

Equations

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

def Duper.mkDatatypeAcyclicityProof (removedLitNum : Nat) (litSide : LitSide) (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.datatypeAcyclicity : MSimpRule

Implements the acyclicity rules described in section 6.4 of https://arxiv.org/pdf/1611.02908

Equations

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