Documentation

Std.Tactic.BVDecide.LRAT.Internal.Formula

← Mathematical handbook

This directory contains the current implementation of the LRAT checker that is plugged into the generic LRAT checking loop from LRATChecker and then used in the surface level LRAT checker that is publicly exposed.