inductive Std.Tactic.BVDecide.LRAT.Internal.Result : Type

• success: Std.Tactic.BVDecide.LRAT.Internal.Result
• outOfProof: Std.Tactic.BVDecide.LRAT.Internal.Result
• rupFailure: Std.Tactic.BVDecide.LRAT.Internal.Result

instance Std.Tactic.BVDecide.LRAT.Internal.instInhabitedResult : Inhabited Std.Tactic.BVDecide.LRAT.Internal.Result

Equations

• Std.Tactic.BVDecide.LRAT.Internal.instInhabitedResult = { default := Std.Tactic.BVDecide.LRAT.Internal.Result.success }

instance Std.Tactic.BVDecide.LRAT.Internal.instDecidableEqResult : DecidableEq Std.Tactic.BVDecide.LRAT.Internal.Result

Equations

• Std.Tactic.BVDecide.LRAT.Internal.instDecidableEqResult x y = if h : x.toCtorIdx = y.toCtorIdx then isTrue ⋯ else isFalse ⋯

instance Std.Tactic.BVDecide.LRAT.Internal.instToStringResult : ToString Std.Tactic.BVDecide.LRAT.Internal.Result

Equations

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

def Std.Tactic.BVDecide.LRAT.Internal.lratChecker {α : Type u_1} {β : Type u_2} {σ : Type u_3} [DecidableEq α] [Std.Tactic.BVDecide.LRAT.Internal.Clause α β] [Std.Tactic.BVDecide.LRAT.Internal.Entails α σ] [Std.Tactic.BVDecide.LRAT.Internal.Formula α β σ] (f : σ) (prf : List (Std.Tactic.BVDecide.LRAT.Action β α)) : Std.Tactic.BVDecide.LRAT.Internal.Result

Equations

• One or more equations did not get rendered due to their size.
• Std.Tactic.BVDecide.LRAT.Internal.lratChecker f [] = Std.Tactic.BVDecide.LRAT.Internal.Result.outOfProof