Documentation

Std.Tactic.BVDecide.LRAT.Internal.Formula.Instance

This module couples the default LRAT implementation to the Formula typeclass.

source
instance Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.instFormulaPosFinDefaultClause {n : Nat} :
Std.Tactic.BVDecide.LRAT.Internal.Formula (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) (Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n)
Equations
  • One or more equations did not get rendered due to their size.