This module contains the implementation of the pre processing pass for automatically splitting up structures containing information about supported types into individual parts recursively.

The implementation operates on all "interesting" types where a type is interesting if it is a non recursive structure and at least one of the following conditions hold:

• it contains something of type BitVec/UIntX/IntX/Bool
• it is parametrized by an interesting type
• it contains another interesting type

For these it:

1. Iterates over all variables in the local context that have an interesting type. For these it recursively asserts all of the contained hypotheses as local facts
2. It post-processes with a custom simp-set that:
   • runs ext_iff lemmas if available in order to handle equality on structures
   • runs simprocs to bubble applications of projections onto control flow operators such as ite or cond into the control flow

def Lean.Meta.Tactic.BVDecide.Normalize.addStructureSimpLemmas (simprocs : Simprocs) (theorems : SimpTheoremsArray) : PreProcessM (Simprocs × SimpTheoremsArray)

Add simp lemmas that we want to apply to structures that we find interesting to simprocs and theorems.

Equations

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

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

Equations

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