Documentation

Std.Tactic.BVDecide.LRAT.Internal.Formula.Class

This module contains the definition of the Formula typeclass. It is the interface that needs to be satisfied by any LRAT implementation that can be used by the generic LRATChecker module.

Typeclass for formulas. An instance [Formula α β σ] indicates that σ is the type of a formula with variables of type α, clauses of type β, and clause ids of type Nat.

Instances