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.applyIteSimproc : Meta.Simp.Simproc

Equations

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

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.applyCondSimproc : Meta.Simp.Simproc

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) (interesting : Std.HashSet Name) : PreProcessM (Option MVarId)

Equations

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

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.structuresPass.mkDiscrPathFor (struct : Name) (structParams projIdx : Nat) (controlFlow : Name) (controlFlowParams : Nat) : Array Meta.DiscrTree.Key

For Prod.fst and ite this function creates the path: Prod.fst (ite (Prod _ _) _ _ _ _). This path can be used to match on applications of structure projections onto control flow primitives.

Equations

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