This file implements the type analysis pass for the structures and enum inductives pass. It figures out which types and matches that occur either directly or transitively (e.g. through being contained in a structure) qualify for further treatment by the structures or enum pass.

source
def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.isSupportedMatch (declName : Name) :
MetaM (Option MatchKind)

Determine whether `declName` is an enum inductive `.match_x` definition that is supported, see `MatchKind` for the supported shapes.

Equations

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

Instances For

source
def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.builtinTypes :
Array Name
Equations

- Lean.Elab.Tactic.BVDecide.Frontend.Normalize.builtinTypes = #[`BitVec, `Bool, `UInt8, `UInt16, `UInt32, `UInt64, `USize, `Int8, `Int16, `Int32, `Int64, `ISize]

Instances For

source
@[inline]
def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.isBuiltIn (n : Name) :
Bool
Equations

- Lean.Elab.Tactic.BVDecide.Frontend.Normalize.isBuiltIn n = Lean.Elab.Tactic.BVDecide.Frontend.Normalize.builtinTypes.contains n

Instances For

source
def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.addDefaultTypeAnalysisLemmas (lemmas : Meta.SimpTheoremsArray) :
PreProcessM Meta.SimpTheoremsArray
Equations

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

Instances For

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

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

Instances For