def Duper.mkPositiveSimplifyReflectProof (mainPremisePos : ClausePos) (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.mkNegativeSimplifyReflectProof (mainPremiseLitIdx : Nat) (mainPremiseLhs : LitSide) (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.forwardPositiveSimplifyReflectWithPartner (mainPremise : MClause) (mainPremiseMVarIds : Array Lean.MVarId) (mainPremisePos : ClausePos) (sidePremise : Clause) : RuleM.RuleM (Option (Array (Clause × RuleM.Proof)))

Checks that (getAtPos mainPremiseLit.lhs mainPremisePos.pos) can be matched with sidePremise[0].sidePremiseLhs and that (getAtPos mainPremiseLit.rhs mainPremisePos.pos) can be matched with sidePremise[0].sidePremiseRhs. Importantly, this function does NOT check mainPremise[pos.lit].sign or that mainPremise[pos.lit].lhs and mainPremise[pos.lit].rhs agree outside of the given pos.

Equations

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

def Duper.forwardPositiveSimplifyReflectAtExpr (mainPremise : MClause) (pos : ClausePos) (potentialSideClauses : Array Clause) (mainMVarIds : Array Lean.MVarId) : RuleM.RuleM (Option (Array (Clause × RuleM.Proof)))

Equations

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

def Duper.forwardPositiveSimplifyReflect (subsumptionTrie : SubsumptionTrie) : MSimpRule

Performs positive simplifyReflect with the given clause c as the main clause

Equations

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

def Duper.forwardNegativeSimplifyReflectWithPartner (mainPremise : MClause) (mainPremiseMVarIds : Array Lean.MVarId) (sidePremise : Clause) (mainPremiseLitIdx : Nat) (mainPremiseLhs : LitSide) : RuleM.RuleM (Option (Array (Clause × RuleM.Proof)))

Equations

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

def Duper.forwardNegativeSimplifyReflectAtLit (subsumptionTrie : SubsumptionTrie) (mainPremise : MClause) (mainPremiseMVarIds : Array Lean.MVarId) (mainPremiseLit : Nat) : RuleM.RuleM (Option (Array (Clause × RuleM.Proof)))

Equations

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

def Duper.forwardNegativeSimplifyReflect (subsumptionTrie : SubsumptionTrie) : MSimpRule

Performs negative simplifyReflect with the given clause c as the main clause

Equations

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

def Duper.backwardPositiveSimplifyReflect (subsumptionTrie : SubsumptionTrie) : BackwardMSimpRule

Performs positive simplifyReflect with the given clause as the side clause

Equations

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

def Duper.backwardNegativeSimplifyReflect (subsumptionTrie : SubsumptionTrie) : BackwardMSimpRule

Performs negative simplifyReflect with the given clause as the side clause

Equations

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