This directory contains the implementation of the LRAT trimming algorithms. It lives here because it uses datastructures and parsing infrastructure from Lean. Otherwise they could be put into Std.Tactic.BVDecide.LRAT.