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 Result
    Equations
      source
      instance Std.Tactic.BVDecide.LRAT.Internal.instDecidableEqResult :
      DecidableEq Result
      Equations
        source
        instance Std.Tactic.BVDecide.LRAT.Internal.instToStringResult :
        ToString Result
        Equations
          source
          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
            Instances For