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

structure Lean.Elab.Tactic.BVDecide.Frontend.Normalize.InterestingStructures : Type

Contains a cache for interesting and uninteresting types such that we don't duplicate work in the structures pass.

• interesting : Std.HashSet Name
• uninteresting : Std.HashSet Name

@[inline]

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.M.lookup (n : Name) : Lean.Elab.Tactic.BVDecide.Frontend.Normalize.M✝ (Option Bool)

Equations

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

@[inline]

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.M.markInteresting (n : Name) : Lean.Elab.Tactic.BVDecide.Frontend.Normalize.M✝ Unit

Equations

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

@[inline]

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.M.markUninteresting (n : Name) : Lean.Elab.Tactic.BVDecide.Frontend.Normalize.M✝ Unit

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.checkContext (goal : MVarId) : Lean.Elab.Tactic.BVDecide.Frontend.Normalize.M✝ Unit

Equations

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

partial def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.structuresPass.constInterestingCached (n : Name) : Lean.Elab.Tactic.BVDecide.Frontend.Normalize.M✝ Bool

partial def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.structuresPass.constInteresting (n : Name) : Lean.Elab.Tactic.BVDecide.Frontend.Normalize.M✝ Bool

partial def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.structuresPass.typeInteresting (expr : Expr) : Lean.Elab.Tactic.BVDecide.Frontend.Normalize.M✝ Bool