This module implements an LRAT checker that acts on an Array IntAction and only explodes it into the DefaultClauseAction when required instead of upfront. This allows for a significantly smaller memory footprint compared to the generic LRAT checker.

def Std.Tactic.BVDecide.LRAT.Internal.compactLratChecker {n : Nat} (f : DefaultFormula n) (proof : Array IntAction) : Result

@[irreducible]

def Std.Tactic.BVDecide.LRAT.Internal.compactLratChecker.go {n : Nat} (f : DefaultFormula n) (proof : Array IntAction) (idx : Nat) : Result