Documentation

Std.Tactic.BVDecide.LRAT.Actions

This module contains the definition of the LRAT format (https://www.cs.utexas.edu/~marijn/publications/lrat.pdf) as a type Action, that is polymorphic over the variables used in the CNF. The type IntAction := Action (Array Int) Nat is the version that is used by the checker as input and should be considered the parsing target for LRAT proofs.

inductive Std.Tactic.BVDecide.LRAT.Action (β : Type u) (α : Type v) :
Type (max u v)

β is for the type of a clause, α is for the type of variables

Instances For
    Equations
    instance Std.Tactic.BVDecide.LRAT.instBEqAction :
    {β : Type u_1} → {α : Type u_2} → [inst : BEq β] → [inst : BEq α] → BEq (Std.Tactic.BVDecide.LRAT.Action β α)
    Equations
    • Std.Tactic.BVDecide.LRAT.instBEqAction = { beq := Std.Tactic.BVDecide.LRAT.beqAction✝ }
    instance Std.Tactic.BVDecide.LRAT.instReprAction :
    {β : Type u_1} → {α : Type u_2} → [inst : Repr β] → [inst : Repr α] → Repr (Std.Tactic.BVDecide.LRAT.Action β α)
    Equations
    • Std.Tactic.BVDecide.LRAT.instReprAction = { reprPrec := Std.Tactic.BVDecide.LRAT.reprAction✝ }
    Equations
    Instances For
      Equations
      • Std.Tactic.BVDecide.LRAT.instToStringAction = { toString := Std.Tactic.BVDecide.LRAT.Action.toString }
      @[reducible, inline]

      Action where variables are (positive) Nat, clauses are arrays of Int, and ids are Nat. This Action type is meant to be a convenient target for parsing LRAT proofs.

      Equations
      Instances For