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 runs cases recursively 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 Afterwards we also:
• apply relevant injEq theorems to support at least equality for these types out of the box.
• push projections of relevant types inside of ite and cond.

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

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

Equations

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

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.structuresPass : Pass

Equations

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

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.structuresPass.postprocess (goal : MVarId) : PreProcessM (Option MVarId)

Equations

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