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

• success : Result
• outOfProof : Result
• rupFailure : Result

Instances For

• Std.Tactic.BVDecide.LRAT.Internal.instInhabitedResult
• Std.Tactic.BVDecide.LRAT.Internal.instToStringResult

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

Equations

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

instance Std.Tactic.BVDecide.LRAT.Internal.instDecidableEqResult : DecidableEq 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 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 α] [Clause α β] [Entails α σ] [Formula α β σ] (f : σ) (prf : List (Action β α)) : 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