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} :
Formula (PosFin n) (DefaultClause n) (DefaultFormula n)
Equations
  • One or more equations did not get rendered due to their size.