This module contains the implementation of the pre processing pass for handling equality on enum inductive types.

The implementation generates mappings from enum inductives occuring in the goal to sufficiently large BitVec and replaces equality on the enum inductives with equality on these mapping functions.

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.enumToBitVecSuffix : String

Equations

• Lean.Elab.Tactic.BVDecide.Frontend.Normalize.enumToBitVecSuffix = "enumToBitVec"

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.eqIffEnumToBitVecEqSuffix : String

Equations

• Lean.Elab.Tactic.BVDecide.Frontend.Normalize.eqIffEnumToBitVecEqSuffix = "eq_iff_enumToBitVec_eq"

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.enumToBitVecLeSuffix : String

Equations

• Lean.Elab.Tactic.BVDecide.Frontend.Normalize.enumToBitVecLeSuffix = "enumToBitVec_le"

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.getEnumToBitVecFor (declName : Name) : MetaM Name

Assuming that declName is an enum inductive construct a function of type declName → BitVec w that maps declName constructors to their numeric indices as BitVec.

Equations

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

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.getEqIffEnumToBitVecEqFor (declName : Name) : MetaM Name

Assuming that declName is an enum inductive, construct a proof of ∀ (x y : declName) : x = y ↔ x.enumToBitVec = y.enumToBitVec.

Equations

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

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.getEqIffEnumToBitVecEqFor.mkInverse {w : Nat} (input retType instBEq : Expr) (ctors : List Name) (counter : BitVec w) (acc : Expr) : Expr

Equations

• One or more equations did not get rendered due to their size.
• Lean.Elab.Tactic.BVDecide.Frontend.Normalize.getEqIffEnumToBitVecEqFor.mkInverse input retType instBEq [] counter acc = acc

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.getEnumToBitVecLeFor (declName : Name) : MetaM Name

Assuming that declName is an enum inductive, construct a proof of ∀ (x : declName) : x.enumToBitVec ≤ domainSize - 1 where domainSize is the amount of constructors of declName.

Equations

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

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

Equations

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

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.enumsPass : Pass

Equations

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

def Lean.Elab.Tactic.BVDecide.Frontend.Normalize.enumsPass.postprocess (goal : MVarId) : StateRefT' IO.RealWorld (Array Meta.Hypothesis) MetaM MVarId

Equations

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