def Duper.isDecidablyFalse (lit : Lit) : Lean.MetaM Bool

Checks whether a literal is decidably false. Returns true if the literal is decidably false and false otherwise.

Equations

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

def Duper.mkDecElimProof (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.decElim : MSimpRule

If there are any literals in c that are decidably true, then decElim removes c. Otherwise, if there are any literals in c that are decidably false, then decElim yields the clause obtained by removing all such literals.

Equations

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