This module contains the implementation of the pre processing pass for handling enum inductive types.

The implementation:

1. generates mappings from enum inductives occurring in the goal to sufficiently large BitVec and replaces equality on the enum inductives with equality on these mapping functions.
2. Constant folds these mappings if appropriate.
3. Adds bounds on the values returned by the mappings if the size of the enum inductive does not fit into a power of two.
4. Handles applications of these mappings to ite, cond and basic match statements.

def Lean.Meta.Tactic.BVDecide.Normalize.enumToBitVecSuffix : String

Equations

• Lean.Meta.Tactic.BVDecide.Normalize.enumToBitVecSuffix = "enumToBitVec"

def Lean.Meta.Tactic.BVDecide.Normalize.enumsPass : Pass

Equations

• One or more equations did not get rendered due to their size.