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.