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`.

source
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.

Instances For

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

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

Instances For