def Duper.is_var (e : Lean.Expr) : Bool

Equations

• Duper.is_var e = match e.consumeMData with | Lean.Expr.mvar mvarId => true | Lean.Expr.fvar fvarId => true | Lean.Expr.bvar deBruijnIndex => true | x => false

def Duper.mkDestructiveEqualtiyResolutionProof (i : 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.destructiveEqualityResolutionAtLit (c : MClause) (i : Nat) : RuleM.RuleM (Option (Clause × RuleM.Proof))

Equations

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

def Duper.destructiveEqualityResolution : MSimpRule

Equations

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