This module contains the basic preprocessing pipeline framework for bv_normalize.

@[inline]

def Lean.Meta.Tactic.BVDecide.Normalize.withDoneResult {m : Type → Type} [Monad m] (x : m Sym.Simp.Result) : m Sym.Simp.Result

Equations

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

inductive Lean.Meta.Tactic.BVDecide.Normalize.Target : Type

• mvarIdTarget (mvar : MVarId) : Target
• grindTarget (goal : Grind.Goal) : Target

@[instance_reducible]

instance Lean.Meta.Tactic.BVDecide.Normalize.instInhabitedTarget : Inhabited Target

Equations

• Lean.Meta.Tactic.BVDecide.Normalize.instInhabitedTarget = { default := Lean.Meta.Tactic.BVDecide.Normalize.instInhabitedTarget.default }

def Lean.Meta.Tactic.BVDecide.Normalize.Target.mvarId : Target → MVarId

Equations

• (Lean.Meta.Tactic.BVDecide.Normalize.Target.mvarIdTarget mvar).mvarId = mvar
• (Lean.Meta.Tactic.BVDecide.Normalize.Target.grindTarget goal).mvarId = goal.mvarId

def Lean.Meta.Tactic.BVDecide.Normalize.Target.isGrind : Target → Bool

Equations

• (Lean.Meta.Tactic.BVDecide.Normalize.Target.mvarIdTarget mvar).isGrind = false
• (Lean.Meta.Tactic.BVDecide.Normalize.Target.grindTarget goal).isGrind = true

def Lean.Meta.Tactic.BVDecide.Normalize.Target.isMVar : Target → Bool

Equations

• (Lean.Meta.Tactic.BVDecide.Normalize.Target.mvarIdTarget mvar).isMVar = true
• (Lean.Meta.Tactic.BVDecide.Normalize.Target.grindTarget goal).isMVar = false

inductive Lean.Meta.Tactic.BVDecide.Normalize.MatchKind : Type

The various kinds of matches supported by the match to cond infrastructure.

• simpleEnum (info : InductiveVal) (ctors : Array ConstructorVal) : MatchKind

  It is a full match statement on an enum inductive with one constructor handled per arm. The ctors are listed in the order they occur in the match statement in ctors.

• enumWithDefault (info : InductiveVal) (ctors : Array ConstructorVal) : MatchKind

  It is a match statement on an enum inductive with a default arm, all explicitly handled ctors are listed in ctors in the order they occur in the match statement.

def Lean.Meta.Tactic.BVDecide.Normalize.MatchKind.getEnumInfo : MatchKind → InductiveVal

The enum inductive that the match discriminates on.

Equations

• (Lean.Meta.Tactic.BVDecide.Normalize.MatchKind.simpleEnum info ctors).getEnumInfo = info
• (Lean.Meta.Tactic.BVDecide.Normalize.MatchKind.enumWithDefault info ctors).getEnumInfo = info

structure Lean.Meta.Tactic.BVDecide.Normalize.TypeAnalysis : Type

Contains the result of the type analysis to be used in the structures and enums pass.

• interestingStructures : Std.HashSet Name

  Structures that are interesting for the structures pass.

• interestingEnums : Std.HashSet Name

  Inductives enums that are interesting for the enums pass.

• interestingMatchers : Std.HashMap Name MatchKind

  func.match_x auxiliary declarations that we consider interesting.

• uninteresting : Std.HashSet Name

  Other types that we've seen that are not interesting, currently only used as a cache.

inductive Lean.Meta.Tactic.BVDecide.Normalize.HypSource : Type

• lctx (fvar : FVarId) : HypSource
• enumDomain (n : Name) : HypSource
• structureProjection (e : Expr) : HypSource
• andFlattened (s : HypSource) : HypSource
• grind : HypSource

@[instance_reducible]

instance Lean.Meta.Tactic.BVDecide.Normalize.instInhabitedHypSource : Inhabited HypSource

Equations

• Lean.Meta.Tactic.BVDecide.Normalize.instInhabitedHypSource = { default := Lean.Meta.Tactic.BVDecide.Normalize.instInhabitedHypSource.default }

@[instance_reducible]

instance Lean.Meta.Tactic.BVDecide.Normalize.instHashableHypSource : Hashable HypSource

Equations

• Lean.Meta.Tactic.BVDecide.Normalize.instHashableHypSource = { hash := Lean.Meta.Tactic.BVDecide.Normalize.instHashableHypSource.hash }

def Lean.Meta.Tactic.BVDecide.Normalize.instHashableHypSource.hash : HypSource → UInt64

Equations

• Lean.Meta.Tactic.BVDecide.Normalize.instHashableHypSource.hash (Lean.Meta.Tactic.BVDecide.Normalize.HypSource.lctx a) = mixHash 0 (hash a)
• Lean.Meta.Tactic.BVDecide.Normalize.instHashableHypSource.hash (Lean.Meta.Tactic.BVDecide.Normalize.HypSource.enumDomain a) = mixHash 1 (hash a)
• Lean.Meta.Tactic.BVDecide.Normalize.instHashableHypSource.hash (Lean.Meta.Tactic.BVDecide.Normalize.HypSource.structureProjection a) = mixHash 2 (hash a)
• Lean.Meta.Tactic.BVDecide.Normalize.instHashableHypSource.hash a.andFlattened = mixHash 3 (Lean.Meta.Tactic.BVDecide.Normalize.instHashableHypSource.hash a)
• Lean.Meta.Tactic.BVDecide.Normalize.instHashableHypSource.hash Lean.Meta.Tactic.BVDecide.Normalize.HypSource.grind = 4

def Lean.Meta.Tactic.BVDecide.Normalize.instBEqHypSource.beq : HypSource → HypSource → Bool

Equations

• One or more equations did not get rendered due to their size.
• Lean.Meta.Tactic.BVDecide.Normalize.instBEqHypSource.beq (Lean.Meta.Tactic.BVDecide.Normalize.HypSource.lctx a) (Lean.Meta.Tactic.BVDecide.Normalize.HypSource.lctx b) = (a == b)
• Lean.Meta.Tactic.BVDecide.Normalize.instBEqHypSource.beq (Lean.Meta.Tactic.BVDecide.Normalize.HypSource.enumDomain a) (Lean.Meta.Tactic.BVDecide.Normalize.HypSource.enumDomain b) = (a == b)
• Lean.Meta.Tactic.BVDecide.Normalize.instBEqHypSource.beq a.andFlattened b.andFlattened = Lean.Meta.Tactic.BVDecide.Normalize.instBEqHypSource.beq a b
• Lean.Meta.Tactic.BVDecide.Normalize.instBEqHypSource.beq Lean.Meta.Tactic.BVDecide.Normalize.HypSource.grind Lean.Meta.Tactic.BVDecide.Normalize.HypSource.grind = true
• Lean.Meta.Tactic.BVDecide.Normalize.instBEqHypSource.beq x✝¹ x✝ = false

@[instance_reducible]

instance Lean.Meta.Tactic.BVDecide.Normalize.instBEqHypSource : BEq HypSource

Equations

• Lean.Meta.Tactic.BVDecide.Normalize.instBEqHypSource = { beq := Lean.Meta.Tactic.BVDecide.Normalize.instBEqHypSource.beq }

@[instance_reducible]

instance Lean.Meta.Tactic.BVDecide.Normalize.instToMessageDataHypSource : ToMessageData HypSource

Equations

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

partial def Lean.Meta.Tactic.BVDecide.Normalize.instToMessageDataHypSource.go (s : HypSource) : MessageData

partial def Lean.Meta.Tactic.BVDecide.Normalize.instToMessageDataHypSource.stripFlatten (s : HypSource) : HypSource

structure Lean.Meta.Tactic.BVDecide.Normalize.Hyp : Type

• name : Name
• type : Expr
• value : Expr
• source : HypSource

@[instance_reducible]

instance Lean.Meta.Tactic.BVDecide.Normalize.instInhabitedHyp : Inhabited Hyp

Equations

• Lean.Meta.Tactic.BVDecide.Normalize.instInhabitedHyp = { default := Lean.Meta.Tactic.BVDecide.Normalize.instInhabitedHyp.default }

@[instance_reducible]

instance Lean.Meta.Tactic.BVDecide.Normalize.instBEqHyp : BEq Hyp

Equations

• Lean.Meta.Tactic.BVDecide.Normalize.instBEqHyp = { beq := fun (lhs rhs : Lean.Meta.Tactic.BVDecide.Normalize.Hyp) => lhs.type == rhs.type }

@[instance_reducible]

instance Lean.Meta.Tactic.BVDecide.Normalize.instHashableHyp : Hashable Hyp

Equations

• Lean.Meta.Tactic.BVDecide.Normalize.instHashableHyp = { hash := fun (hyp : Lean.Meta.Tactic.BVDecide.Normalize.Hyp) => hash hyp.type }

@[instance_reducible]

instance Lean.Meta.Tactic.BVDecide.Normalize.instToMessageDataHyp : ToMessageData Hyp

Equations

• Lean.Meta.Tactic.BVDecide.Normalize.instToMessageDataHyp = { toMessageData := fun (hyp : Lean.Meta.Tactic.BVDecide.Normalize.Hyp) => Lean.toMessageData hyp.type }

inductive Lean.Meta.Tactic.BVDecide.Normalize.Mode : Type

The mode that the bv_normalize preprocessing pipeline runs in.

• solve (restrictedTypes : Option (Array Name)) : Mode

  A regular run as part of bv_decide or a standalone bv_normalize. restrictedTypes are the types that the structure and enum analysis is restricted to, as provided by the types clause. If this is none the analysis discovers the relevant types on its own.

• push : Mode

  A run as part of bv_decide_push. It merely prepares the caches of the passes for later runs of the pipeline on descendants of this goal and may thus only produce context independent information.

def Lean.Meta.Tactic.BVDecide.Normalize.Mode.isPush : Mode → Bool

Equations

• Lean.Meta.Tactic.BVDecide.Normalize.Mode.push.isPush = true
• (Lean.Meta.Tactic.BVDecide.Normalize.Mode.solve restrictedTypes).isPush = false

def Lean.Meta.Tactic.BVDecide.Normalize.Mode.restrictedTypes : Mode → Option (Array Name)

Equations

• (Lean.Meta.Tactic.BVDecide.Normalize.Mode.solve types).restrictedTypes = types
• Lean.Meta.Tactic.BVDecide.Normalize.Mode.push.restrictedTypes = none

def Lean.Meta.Tactic.BVDecide.Normalize.Mode.adjustConfig (mode : Mode) (config : Elab.Tactic.BVDecide.BVDecideConfig) : Elab.Tactic.BVDecide.BVDecideConfig

Disables the configuration options that mode cannot support. In push mode these are the options that either depend on the context (e.g. enums, structures) or require a more clever incrementality scheme (e.g. embeddedConstraintSubst, andFlattening).

Equations

• One or more equations did not get rendered due to their size.
• (Lean.Meta.Tactic.BVDecide.Normalize.Mode.solve types).adjustConfig config = config

structure Lean.Meta.Tactic.BVDecide.Normalize.PreProcessContext : Type

The immutable context of the bv_normalize preprocessing pipeline. Use PreProcessContext.new to create one.

• config : Elab.Tactic.BVDecide.BVDecideConfig

  The configuration that the tactic was called with, already adjusted for mode.

• mode : Mode

  The mode that the pipeline runs in.

def Lean.Meta.Tactic.BVDecide.Normalize.PreProcessContext.new (mode : Mode) (config : Elab.Tactic.BVDecide.BVDecideConfig) : PreProcessContext

Creates the context for a run of the pipeline in mode, disabling all configuration options that mode does not support.

Equations

• Lean.Meta.Tactic.BVDecide.Normalize.PreProcessContext.new mode config = { config := mode.adjustConfig config, mode := mode }

inductive Lean.Meta.Tactic.BVDecide.Normalize.SimpCacheId : Type

Identifies the Sym.Simp cache that a pass operates on.

• rewrite : SimpCacheId
• ac : SimpCacheId

inductive Lean.Meta.Tactic.BVDecide.Normalize.DSimpCacheId : Type

Identifies the Sym.DSimp cache that a pass operates on.

• rewrite : DSimpCacheId
• reduction : DSimpCacheId

def Lean.Meta.Tactic.BVDecide.Normalize.SimpCacheId.get : SimpCacheId → Grind.BVDecide.Caches → Sym.Simp.Cache

Equations

• Lean.Meta.Tactic.BVDecide.Normalize.SimpCacheId.rewrite.get x✝ = x✝.rewriteSimp
• Lean.Meta.Tactic.BVDecide.Normalize.SimpCacheId.ac.get x✝ = x✝.ac

def Lean.Meta.Tactic.BVDecide.Normalize.SimpCacheId.set : SimpCacheId → Sym.Simp.Cache → Grind.BVDecide.Caches → Grind.BVDecide.Caches

Equations

• Lean.Meta.Tactic.BVDecide.Normalize.SimpCacheId.rewrite.set x✝¹ x✝ = { reduction := x✝.reduction, rewriteSimp := x✝¹, rewriteDSimp := x✝.rewriteDSimp, ac := x✝.ac }
• Lean.Meta.Tactic.BVDecide.Normalize.SimpCacheId.ac.set x✝¹ x✝ = { reduction := x✝.reduction, rewriteSimp := x✝.rewriteSimp, rewriteDSimp := x✝.rewriteDSimp, ac := x✝¹ }

def Lean.Meta.Tactic.BVDecide.Normalize.DSimpCacheId.get : DSimpCacheId → Grind.BVDecide.Caches → Sym.DSimp.Cache

Equations

• Lean.Meta.Tactic.BVDecide.Normalize.DSimpCacheId.rewrite.get x✝ = x✝.rewriteDSimp
• Lean.Meta.Tactic.BVDecide.Normalize.DSimpCacheId.reduction.get x✝ = x✝.reduction

def Lean.Meta.Tactic.BVDecide.Normalize.DSimpCacheId.set : DSimpCacheId → Sym.DSimp.Cache → Grind.BVDecide.Caches → Grind.BVDecide.Caches

Equations

• Lean.Meta.Tactic.BVDecide.Normalize.DSimpCacheId.rewrite.set x✝¹ x✝ = { reduction := x✝.reduction, rewriteSimp := x✝.rewriteSimp, rewriteDSimp := x✝¹, ac := x✝.ac }
• Lean.Meta.Tactic.BVDecide.Normalize.DSimpCacheId.reduction.set x✝¹ x✝ = { reduction := x✝¹, rewriteSimp := x✝.rewriteSimp, rewriteDSimp := x✝.rewriteDSimp, ac := x✝.ac }

structure Lean.Meta.Tactic.BVDecide.Normalize.PreProcessState : Type

• caches : Grind.BVDecide.Caches

  The caches of the passes that maintain one.

• typeAnalysis : TypeAnalysis

  Analysis results for the structure and enum pass if required.

• target : Target

  The target we are operating on.

• hypotheses : Array Hyp

  The set of hypotheses we are operating on. These should be interpreted from withing the lctx of the goal. But they may not necessarily be fvars registered in the goal.

• didChange : Bool

  A didChange flag for our fixpoint simplification loop.

@[reducible, inline]

abbrev Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM : Type → Type

Equations

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

def Lean.Meta.Tactic.BVDecide.Normalize.Hyp.applySimpResult (hyp : Hyp) (result : Sym.Simp.Result) : Sym.SymM Hyp

Equations

• One or more equations did not get rendered due to their size.
• hyp.applySimpResult (Lean.Meta.Sym.Simp.Result.rfl done dep) = pure hyp

def Lean.Meta.Tactic.BVDecide.Normalize.Hyp.applyDSimpResult (hyp : Hyp) (result : Sym.DSimp.Result) : Sym.SymM Hyp

Equations

• hyp.applyDSimpResult result = pure { name := hyp.name, type := Lean.Meta.Sym.DSimp.Result.getResultExpr hyp.type result, value := hyp.value, source := hyp.source }

@[inline]

def Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.getConfig : PreProcessM Elab.Tactic.BVDecide.BVDecideConfig

Equations

• Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.getConfig = do let __do_lift ← read pure __do_lift.config

@[inline]

def Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.getRestrictedTypes : PreProcessM (Option (Array Name))

Equations

• Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.getRestrictedTypes = do let __do_lift ← read pure __do_lift.mode.restrictedTypes

@[inline]

def Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.isPushMode : PreProcessM Bool

Equations

• Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.isPushMode = do let __do_lift ← read pure __do_lift.mode.isPush

@[inline]

def Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.getTarget : PreProcessM Target

Equations

• Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.getTarget = do let __do_lift ← get pure __do_lift.target

@[inline]

def Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.getTargetMVarId : PreProcessM MVarId

Equations

• Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.getTargetMVarId = do let __do_lift ← get pure __do_lift.target.mvarId

@[inline]

def Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.setTarget (target : Target) : PreProcessM Unit

Equations

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

@[inline]

def Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.withGrindGoal {α : Type} (x : Grind.GoalM α) : PreProcessM (Option α)

Runs x on the target if it is a grind goal and writes the updated goal back. Returns none if the target is a plain MVarId.

Equations

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

def Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.closeTarget (falseProof : Expr) : PreProcessM Unit

Closes the target using falseProof : False. Grind targets are additionally marked as inconsistent so that grind knows that there is nothing left to do for this goal.

Equations

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

@[inline]

def Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.didChange : PreProcessM Bool

Equations

• Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.didChange = do let __do_lift ← get pure __do_lift.didChange

@[inline]

def Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.resetDidChange : PreProcessM Unit

Equations

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

@[inline]

def Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.setDidChange : PreProcessM Unit

Equations

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

@[inline]

def Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.getCaches : PreProcessM Grind.BVDecide.Caches

Equations

• Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.getCaches = do let __do_lift ← get pure __do_lift.caches

@[inline]

def Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.setCaches (caches : Grind.BVDecide.Caches) : PreProcessM Unit

Equations

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

def Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.dropPassCaches : PreProcessM Unit

Drops the caches of all passes that maintain one. In bv_decide_push mode this is a no-op as the caches are the very thing that we want to hand to the next invocation.

Equations

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

@[inline]

def Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.getTypeAnalysis : PreProcessM TypeAnalysis

Equations

• Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.getTypeAnalysis = do let __do_lift ← get pure __do_lift.typeAnalysis

@[inline]

def Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.lookupInterestingStructure (n : Name) : PreProcessM (Option Bool)

Equations

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

@[inline]

def Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.modifyTypeAnalysis (f : TypeAnalysis → TypeAnalysis) : PreProcessM Unit

Equations

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

@[inline]

def Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.markInterestingStructure (n : Name) : PreProcessM Unit

Equations

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

@[inline]

def Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.markInterestingEnum (n : Name) : PreProcessM Unit

Equations

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

@[inline]

def Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.markInterestingMatcher (n : Name) (k : MatchKind) : PreProcessM Unit

Equations

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

@[inline]

def Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.markUninterestingConst (n : Name) : PreProcessM Unit

Equations

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

@[inline]

def Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.run {α : Type} (ctx : PreProcessContext) (target : Target) (x : PreProcessM α) : Grind.GrindM (α × PreProcessState)

Equations

• Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.run ctx target x = (ReaderT.run x ctx).run { target := target }

@[inline]

def Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.run' {α : Type} (ctx : PreProcessContext) (target : Target) (x : PreProcessM α) : Grind.GrindM α

Equations

• Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.run' ctx target x = Prod.fst <$> Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.run ctx target x

@[inline]

def Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.pushHyp (hyp : Hyp) : PreProcessM Unit

Equations

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

@[inline]

def Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.addHyps (hyps : Array Hyp) : PreProcessM Unit

Equations

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

@[inline]

def Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.getHyps : PreProcessM (Array Hyp)

Equations

• Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.getHyps = do let __do_lift ← get pure __do_lift.hypotheses

@[inline]

def Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.flatMapHyps {m : Type → Type} [Monad m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [MonadRef m] [MonadLiftT PreProcessM m] (f : Hyp → m (Array Hyp)) : m Unit

Equations

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

@[inline]

def Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.mapIdxHyps {m : Type → Type} [Monad m] [MonadLiftT PreProcessM m] [MonadError m] [MonadMCtx m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [Sym.Internal.MonadShareCommon m] (f : Nat → Hyp → m Hyp) : m Bool

Equations

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

@[inline]

def Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.mapHyps {m : Type → Type} [Monad m] [MonadLiftT PreProcessM m] [MonadError m] [MonadMCtx m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] [Sym.Internal.MonadShareCommon m] (f : Hyp → m Hyp) : m Bool

Equations

• Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.mapHyps f = Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.mapIdxHyps fun (x : Nat) (hyp : Lean.Meta.Tactic.BVDecide.Normalize.Hyp) => f hyp

@[inline]

def Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.forHyps {m : Type → Type} [Monad m] [MonadLiftT PreProcessM m] [MonadError m] (f : Hyp → m Unit) : m Unit

Equations

• Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.forHyps f = do let hyps ← liftM Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.getHyps Array.forM f hyps

def Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.simpHyp (cacheId : SimpCacheId) (methods : Sym.Simp.Methods) (config : Sym.Simp.Config) (hyp : Hyp) : PreProcessM Hyp

Runs Sym.Simp on hyp, using the cache identified by cacheId and updating it in place.

Equations

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

def Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.dsimpHyp (cacheId : DSimpCacheId) (methods : Sym.DSimp.Methods) (config : Sym.DSimp.Config) (hyp : Hyp) : PreProcessM Hyp

Runs Sym.DSimp on hyp, using the cache identified by cacheId and updating it in place.

Equations

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

@[inline]

def Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.simpHyps (cacheId : SimpCacheId) (methods : Sym.Simp.Methods) (config : Sym.Simp.Config) : PreProcessM Bool

Equations

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

@[inline]

def Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.dsimpHyps (cacheId : DSimpCacheId) (methods : Sym.DSimp.Methods) (config : Sym.DSimp.Config) : PreProcessM Bool

Equations

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

def Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.mapSimpHyps (methods : Sym.Simp.Methods) (config : Sym.Simp.Config) : PreProcessM Bool

Equations

• Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.mapSimpHyps methods config = (Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.mapSimpHyps.go✝ methods config).run' { }

def Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.mapDSimpHyps (methods : Sym.DSimp.Methods) (config : Sym.DSimp.Config) : PreProcessM Bool

Equations

• Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.mapDSimpHyps methods config = (Lean.Meta.Tactic.BVDecide.Normalize.PreProcessM.mapDSimpHyps.go✝ methods config).run' { }

structure Lean.Meta.Tactic.BVDecide.Normalize.Pass : Type

A pass in the normalization pipeline. It operates on the current set of hypotheses stored in the PreProcessM monad. If it manages to find a way to close the associated goal it can indicate so by returning true. Otherwise it should always return false.

• name : Name
• run' : PreProcessM Bool

@[inline]

def Lean.Meta.Tactic.BVDecide.Normalize.Pass.run (pass : Pass) : PreProcessM Bool

Equations

• pass.run = Lean.withTraceNode `Meta.Tactic.bv (fun (x : Except Lean.Exception Bool) => pure (Lean.toMessageData "Running pass: " ++ Lean.toMessageData pass.name)) pass.run'

def Lean.Meta.Tactic.BVDecide.Normalize.Pass.fixpointPipeline (passes : List Pass) : PreProcessM Bool

Repeatedly run a list of Pass until they either close the goal or an iteration doesn't change the goal anymore.

Equations

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