HepLean Documentation

Std.Tactic.BVDecide.LRAT.Internal.Formula

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.