This module contains the implementation of `bv_normalize`

which is effectively a custom `bv_normalize`

simp set that is called like this: `simp only [seval, bv_normalize]`

. The rules in `bv_normalize`

fulfill two goals:

- Turn all hypothesis involving
`Bool`

and`BitVec`

into the form`x = true`

where`x`

only consists of a operations on`Bool`

and`BitVec`

. In particular no`Prop`

should be contained. This makes the reflection procedure further down the pipeline much easier to implement. - Apply simplification rules from the Bitwuzla SMT solver.

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

@[reducible, inline]

A pass in the normalization pipeline. Takes the current goal and produces a refined one or closes
the goal fully, indicated by returning `none`

.

## Equations

## Instances For

partial def
Lean.Elab.Tactic.BVDecide.Frontend.Normalize.Pass.fixpointPipeline
(passes : List Lean.Elab.Tactic.BVDecide.Frontend.Normalize.Pass)
(goal : Lean.MVarId)
:

Repeatedly run a list of `Pass`

until they either close the goal or an iteration doesn't change
the goal anymore.

Responsible for applying the Bitwuzla style rewrite rules.

## Equations

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

## Instances For

The normalization passes used by `bv_normalize`

and thus `bv_decide`

.

## Equations

## Instances For

## Equations

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

## Instances For

## Equations

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