Documentation

Duper.Rules.FalseElim

Determines whether a literal has can be unified with the form False = True or True = False. If it can be, then the substitution necessary to achieve that match is applied (if the match is unsuccessful, then the MCtx remains unchanged)

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    def Duper.mkFalseElimProof (i : Nat) (premises : List Lean.Expr) (parents : List RuleM.ProofParent) (transferExprs : Array Lean.Expr) (c : Clause) :
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

        If there is a substitution σ and literal l in c such that σ(l) equates True and False, then falseElim yields the clause obtained by removing l from c and applying sigma to the rest of c

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