Documentation

Std.Tactic.BVDecide.LRAT.Internal.LRATChecker

source
inductive Std.Tactic.BVDecide.LRAT.Internal.Result :
Type
Instances For
    source
    instance Std.Tactic.BVDecide.LRAT.Internal.instInhabitedResult :
    Inhabited Std.Tactic.BVDecide.LRAT.Internal.Result
    Equations
    source
    instance Std.Tactic.BVDecide.LRAT.Internal.instDecidableEqResult :
    DecidableEq Std.Tactic.BVDecide.LRAT.Internal.Result
    Equations
    source
    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.
    source
    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
    Instances For