def Duper.mkContextualLiteralCuttingProof (negatedLitMainIdx : Nat) (assignment : List (Nat × Bool)) (isForward : Bool) (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.negateMClauseLit (c : MClause) (litIndex : Nat) : RuleM.RuleM MClause

Returns an mclause identical to c except that the lit indicated by litIndex is negated

Equations

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

def Duper.forwardContextualLiteralCuttingWithPartner (mainClauseWithNegatedLit : MClause) (mainClauseMVarIds : Array Lean.MVarId) (sideClause : Clause) (negatedLitIdx : Nat) : RuleM.RuleM (Option (Clause × RuleM.Proof))

Equations

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

def Duper.forwardContextualLiteralCutting (subsumptionTrie : SubsumptionTrie) : MSimpRule

Performs contextual literal cutting with c as the main clause

Equations

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

def Duper.backwardContextualLiteralCuttingWithPartner (sideClauseWithNegatedLit : MClause) (mainClause : Clause) (negatedLitIdx : Nat) : RuleM.RuleM (Option (Clause × RuleM.Proof))

Equations

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

def Duper.backwardContextualLiteralCutting (subsumptionTrie : SubsumptionTrie) : BackwardMSimpRule

Performs contextual literal cutting with the given clause as the side clause

Equations

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