opaque Lean.Meta.Simp.congrHypothesisExceptionId : InternalExceptionId

def Lean.Meta.Simp.throwCongrHypothesisFailed {α : Type} : MetaM α

Equations

• Lean.Meta.Simp.throwCongrHypothesisFailed = throw (Lean.Exception.internal Lean.Meta.Simp.congrHypothesisExceptionId)

def Lean.Meta.Simp.isOfNatNatLit (e : Expr) : Bool

Return true if e is of the form ofNat n where n is a kernel Nat literal

Equations

• Lean.Meta.Simp.isOfNatNatLit e = (e.isAppOf `OfNat.ofNat && decide (e.getAppNumArgs ≥ 3) && (e.getArg! 1).isRawNatLit)

def Lean.Meta.Simp.foldRawNatLit (e : Expr) : SimpM Expr

If e is a raw Nat literal and OfNat.ofNat is not in the list of declarations to unfold, return an OfNat.ofNat-application.

Equations

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

def Lean.Meta.Simp.isOfScientificLit (e : Expr) : Bool

Return true if e is of the form ofScientific n b m where n and m are kernel Nat literals.

Equations

• Lean.Meta.Simp.isOfScientificLit e = (e.isAppOfArity `OfScientific.ofScientific 5 && (e.getArg! 4).isRawNatLit && (e.getArg! 2).isRawNatLit)

def Lean.Meta.Simp.isCharLit (e : Expr) : Bool

Return true if e is of the form Char.ofNat n where n is a kernel Nat literals.

Equations

• Lean.Meta.Simp.isCharLit e = (e.isAppOfArity `Char.ofNat 1 && e.appArg!.isRawNatLit)

instance Lean.Meta.Simp.instInhabitedSimpM {α : Type} : Inhabited (SimpM α)

Equations

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

def Lean.Meta.Simp.lambdaTelescopeDSimp {α : Type} (e : Expr) (k : Array Expr → Expr → SimpM α) : SimpM α

Equations

• Lean.Meta.Simp.lambdaTelescopeDSimp e k = Lean.Meta.Simp.lambdaTelescopeDSimp.go k #[] e

partial def Lean.Meta.Simp.lambdaTelescopeDSimp.go {α : Type} (k : Array Expr → Expr → SimpM α) (xs : Array Expr) (e : Expr) : SimpM α

inductive Lean.Meta.Simp.SimpLetCase : Type

• dep : SimpLetCase
• nondepDepVar : SimpLetCase
• nondep : SimpLetCase

def Lean.Meta.Simp.getSimpLetCase (n : Name) (t b : Expr) : MetaM SimpLetCase

Equations

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

def Lean.Meta.Simp.withNewLemmas {α : Type} (xs : Array Expr) (f : SimpM α) : SimpM α

We use withNewlemmas whenever updating the local context.

Equations

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

def Lean.Meta.Simp.simpProj (e : Expr) : SimpM Result

Equations

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

def Lean.Meta.Simp.simpConst (e : Expr) : SimpM Result

Equations

• Lean.Meta.Simp.simpConst e = do let __do_lift ← Lean.Meta.Simp.reduce✝ e pure { expr := __do_lift, proof? := none, cache := true }

def Lean.Meta.Simp.simpLambda (e : Expr) : SimpM Result

Equations

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

def Lean.Meta.Simp.simpArrow (e : Expr) : SimpM Result

Equations

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

def Lean.Meta.Simp.simpForall (e : Expr) : SimpM Result

Equations

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

def Lean.Meta.Simp.simpLet (e : Expr) : SimpM Result

Equations

• One or more equations did not get rendered due to their size.
• Lean.Meta.Simp.simpLet e = panicWithPosWithDecl "Lean.Meta.Tactic.Simp.Main" "Lean.Meta.Simp.simpLet" 392 29 "unreachable code has been reached"

def Lean.Meta.Simp.visitFn (e : Expr) : SimpM Result

Equations

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

def Lean.Meta.Simp.congrDefault (e : Expr) : SimpM Result

Equations

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

def Lean.Meta.Simp.processCongrHypothesis (h : Expr) : SimpM Bool

Process the given congruence theorem hypothesis. Return true if it made "progress".

Equations

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

def Lean.Meta.Simp.trySimpCongrTheorem? (c : SimpCongrTheorem) (e : Expr) : SimpM (Option Result)

Try to rewrite e children using the given congruence theorem

Equations

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

def Lean.Meta.Simp.congr (e : Expr) : SimpM Result

Equations

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

def Lean.Meta.Simp.isNonDepLetFun (e : Expr) : Bool

Returns true if e is of the form @letFun _ (fun _ => β) _ _

β must not contain loose bound variables. Recall that simp does not have support for let_funs where resulting type depends on the let-value. Example:

let_fun n := 10;
BitVec.zero n

Equations

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

def Lean.Meta.Simp.simpNonDepLetFun (e : Expr) : SimpM Result

Simplifies a sequence of let_fun declarations. It attempts to minimize the quadratic overhead imposed by the locally nameless discipline.

Equations

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

partial def Lean.Meta.Simp.simpNonDepLetFun.go (xs : Array Expr) (e : Expr) : SimpM Lean.Meta.Simp.SimpLetFunResult✝

def Lean.Meta.Simp.simpApp (e : Expr) : SimpM Result

Equations

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

def Lean.Meta.Simp.simpStep (e : Expr) : SimpM Result

Equations

• One or more equations did not get rendered due to their size.
• Lean.Meta.Simp.simpStep (Lean.Expr.mdata m e_2) = do let r ← Lean.Meta.Simp.simp e_2 pure { expr := Lean.mkMData m r.expr, proof? := r.proof?, cache := r.cache }
• Lean.Meta.Simp.simpStep (Lean.Expr.proj typeName idx struct) = Lean.Meta.Simp.simpProj (Lean.Expr.proj typeName idx struct)
• Lean.Meta.Simp.simpStep (fn.app arg) = Lean.Meta.Simp.simpApp (fn.app arg)
• Lean.Meta.Simp.simpStep (Lean.Expr.lam binderName binderType body binderInfo) = Lean.Meta.Simp.simpLambda (Lean.Expr.lam binderName binderType body binderInfo)
• Lean.Meta.Simp.simpStep (Lean.Expr.forallE binderName binderType body binderInfo) = Lean.Meta.Simp.simpForall (Lean.Expr.forallE binderName binderType body binderInfo)
• Lean.Meta.Simp.simpStep (Lean.Expr.letE declName type value body nonDep) = Lean.Meta.Simp.simpLet (Lean.Expr.letE declName type value body nonDep)
• Lean.Meta.Simp.simpStep (Lean.Expr.const declName us) = Lean.Meta.Simp.simpConst (Lean.Expr.const declName us)
• Lean.Meta.Simp.simpStep (Lean.Expr.bvar deBruijnIndex) = panicWithPosWithDecl "Lean.Meta.Tactic.Simp.Main" "Lean.Meta.Simp.simpStep" 721 20 "unreachable code has been reached"
• Lean.Meta.Simp.simpStep (Lean.Expr.sort u) = pure { expr := Lean.Expr.sort u, proof? := none, cache := true }
• Lean.Meta.Simp.simpStep (Lean.Expr.lit a) = pure { expr := Lean.Expr.lit a, proof? := none, cache := true }
• Lean.Meta.Simp.simpStep (Lean.Expr.mvar mvarId) = do let __do_lift ← Lean.instantiateMVars (Lean.Expr.mvar mvarId) pure { expr := __do_lift, proof? := none, cache := true }

def Lean.Meta.Simp.cacheResult (e : Expr) (cfg : Config) (r : Result) : SimpM Result

Equations

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

partial def Lean.Meta.Simp.simpLoop (e : Expr) : SimpM Result

partial def Lean.Meta.Simp.simpLoop.visitPreContinue (e : Expr) (cfg : Config) (r : Result) : SimpM Result

partial def Lean.Meta.Simp.simpLoop.visitPost (e : Expr) (cfg : Config) (r : Result) : SimpM Result

partial def Lean.Meta.Simp.simpLoop.visitPostContinue (e : Expr) (cfg : Config) (r : Result) : SimpM Result

@[export lean_simp]

def Lean.Meta.Simp.simpImpl (e : Expr) : SimpM Result

Equations

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

def Lean.Meta.Simp.simpImpl.go (e : Expr) : SimpM Result

Equations

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

def Lean.Meta.Simp.main (e : Expr) (ctx : Context) (stats : Stats := { usedTheorems := { map := { root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray }, size := 0 }, diag := { usedThmCounter := { root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray }, triedThmCounter := { root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray }, congrThmCounter := { root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray }, thmsWithBadKeys := { root := PersistentArrayNode.node (Array.mkEmpty PersistentArray.branching.toNat), tail := Array.mkEmpty PersistentArray.branching.toNat, size := 0, shift := PersistentArray.initShift, tailOff := 0 } } }) (methods : Methods := { pre := fun (x : Expr) => pure Step.continue, post := fun (e : Expr) => pure (Step.done { expr := e, proof? := none, cache := true }), dpre := fun (x : Expr) => pure TransformStep.continue, dpost := fun (e : Expr) => pure (TransformStep.done e), discharge? := fun (x : Expr) => pure none, wellBehavedDischarge := true }) : MetaM (Result × Stats)

Equations

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

def Lean.Meta.Simp.main.go (e : Expr) : SimpM Result

Equations

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

def Lean.Meta.Simp.dsimpMain (e : Expr) (ctx : Context) (stats : Stats := { usedTheorems := { map := { root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray }, size := 0 }, diag := { usedThmCounter := { root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray }, triedThmCounter := { root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray }, congrThmCounter := { root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray }, thmsWithBadKeys := { root := PersistentArrayNode.node (Array.mkEmpty PersistentArray.branching.toNat), tail := Array.mkEmpty PersistentArray.branching.toNat, size := 0, shift := PersistentArray.initShift, tailOff := 0 } } }) (methods : Methods := { pre := fun (x : Expr) => pure Step.continue, post := fun (e : Expr) => pure (Step.done { expr := e, proof? := none, cache := true }), dpre := fun (x : Expr) => pure TransformStep.continue, dpost := fun (e : Expr) => pure (TransformStep.done e), discharge? := fun (x : Expr) => pure none, wellBehavedDischarge := true }) : MetaM (Expr × Stats)

Equations

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

def Lean.Meta.Simp.dsimpMain.go (e : Expr) : SimpM Expr

Equations

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

def Lean.Meta.simp (e : Expr) (ctx : Simp.Context) (simprocs : Simp.SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none) (stats : Simp.Stats := { usedTheorems := { map := { root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray }, size := 0 }, diag := { usedThmCounter := { root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray }, triedThmCounter := { root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray }, congrThmCounter := { root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray }, thmsWithBadKeys := { root := PersistentArrayNode.node (Array.mkEmpty PersistentArray.branching.toNat), tail := Array.mkEmpty PersistentArray.branching.toNat, size := 0, shift := PersistentArray.initShift, tailOff := 0 } } }) : MetaM (Simp.Result × Simp.Stats)

Equations

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

def Lean.Meta.dsimp (e : Expr) (ctx : Simp.Context) (simprocs : Simp.SimprocsArray := #[]) (stats : Simp.Stats := { usedTheorems := { map := { root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray }, size := 0 }, diag := { usedThmCounter := { root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray }, triedThmCounter := { root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray }, congrThmCounter := { root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray }, thmsWithBadKeys := { root := PersistentArrayNode.node (Array.mkEmpty PersistentArray.branching.toNat), tail := Array.mkEmpty PersistentArray.branching.toNat, size := 0, shift := PersistentArray.initShift, tailOff := 0 } } }) : MetaM (Expr × Simp.Stats)

Equations

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

def Lean.Meta.simpTargetCore (mvarId : MVarId) (ctx : Simp.Context) (simprocs : Simp.SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none) (mayCloseGoal : Bool := true) (stats : Simp.Stats := { usedTheorems := { map := { root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray }, size := 0 }, diag := { usedThmCounter := { root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray }, triedThmCounter := { root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray }, congrThmCounter := { root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray }, thmsWithBadKeys := { root := PersistentArrayNode.node (Array.mkEmpty PersistentArray.branching.toNat), tail := Array.mkEmpty PersistentArray.branching.toNat, size := 0, shift := PersistentArray.initShift, tailOff := 0 } } }) : MetaM (Option MVarId × Simp.Stats)

See simpTarget. This method assumes mvarId is not assigned, and we are already using mvarIds local context.

Equations

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

def Lean.Meta.simpTarget (mvarId : MVarId) (ctx : Simp.Context) (simprocs : Simp.SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none) (mayCloseGoal : Bool := true) (stats : Simp.Stats := { usedTheorems := { map := { root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray }, size := 0 }, diag := { usedThmCounter := { root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray }, triedThmCounter := { root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray }, congrThmCounter := { root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray }, thmsWithBadKeys := { root := PersistentArrayNode.node (Array.mkEmpty PersistentArray.branching.toNat), tail := Array.mkEmpty PersistentArray.branching.toNat, size := 0, shift := PersistentArray.initShift, tailOff := 0 } } }) : MetaM (Option MVarId × Simp.Stats)

Simplify the given goal target (aka type). Return none if the goal was closed. Return some mvarId' otherwise, where mvarId' is the simplified new goal.

Equations

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

def Lean.Meta.applySimpResultToProp (mvarId : MVarId) (proof prop : Expr) (r : Simp.Result) (mayCloseGoal : Bool := true) : MetaM (Option (Expr × Expr))

Apply the result r for prop (which is inhabited by proof). Return none if the goal was closed. Return some (proof', prop') otherwise, where proof' : prop' and prop' is the simplified prop.

This method assumes mvarId is not assigned, and we are already using mvarIds local context.

Equations

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

def Lean.Meta.applySimpResultToFVarId (mvarId : MVarId) (fvarId : FVarId) (r : Simp.Result) (mayCloseGoal : Bool) : MetaM (Option (Expr × Expr))

Equations

• Lean.Meta.applySimpResultToFVarId mvarId fvarId r mayCloseGoal = do let localDecl ← fvarId.getDecl Lean.Meta.applySimpResultToProp mvarId (Lean.mkFVar fvarId) localDecl.type r mayCloseGoal

def Lean.Meta.simpStep (mvarId : MVarId) (proof prop : Expr) (ctx : Simp.Context) (simprocs : Simp.SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none) (mayCloseGoal : Bool := true) (stats : Simp.Stats := { usedTheorems := { map := { root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray }, size := 0 }, diag := { usedThmCounter := { root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray }, triedThmCounter := { root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray }, congrThmCounter := { root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray }, thmsWithBadKeys := { root := PersistentArrayNode.node (Array.mkEmpty PersistentArray.branching.toNat), tail := Array.mkEmpty PersistentArray.branching.toNat, size := 0, shift := PersistentArray.initShift, tailOff := 0 } } }) : MetaM (Option (Expr × Expr) × Simp.Stats)

Simplify prop (which is inhabited by proof). Return none if the goal was closed. Return some (proof', prop') otherwise, where proof' : prop' and prop' is the simplified prop.

This method assumes mvarId is not assigned, and we are already using mvarIds local context.

Equations

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

def Lean.Meta.applySimpResultToLocalDeclCore (mvarId : MVarId) (fvarId : FVarId) (r : Option (Expr × Expr)) : MetaM (Option (FVarId × MVarId))

Equations

• One or more equations did not get rendered due to their size.
• Lean.Meta.applySimpResultToLocalDeclCore mvarId fvarId none = pure none

def Lean.Meta.applySimpResultToLocalDecl (mvarId : MVarId) (fvarId : FVarId) (r : Simp.Result) (mayCloseGoal : Bool) : MetaM (Option (FVarId × MVarId))

Simplify simp result to the given local declaration. Return none if the goal was closed. This method assumes mvarId is not assigned, and we are already using mvarIds local context.

Equations

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

def Lean.Meta.simpLocalDecl (mvarId : MVarId) (fvarId : FVarId) (ctx : Simp.Context) (simprocs : Simp.SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none) (mayCloseGoal : Bool := true) (stats : Simp.Stats := { usedTheorems := { map := { root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray }, size := 0 }, diag := { usedThmCounter := { root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray }, triedThmCounter := { root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray }, congrThmCounter := { root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray }, thmsWithBadKeys := { root := PersistentArrayNode.node (Array.mkEmpty PersistentArray.branching.toNat), tail := Array.mkEmpty PersistentArray.branching.toNat, size := 0, shift := PersistentArray.initShift, tailOff := 0 } } }) : MetaM (Option (FVarId × MVarId) × Simp.Stats)

Equations

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

def Lean.Meta.simpGoal (mvarId : MVarId) (ctx : Simp.Context) (simprocs : Simp.SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none) (simplifyTarget : Bool := true) (fvarIdsToSimp : Array FVarId := #[]) (stats : Simp.Stats := { usedTheorems := { map := { root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray }, size := 0 }, diag := { usedThmCounter := { root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray }, triedThmCounter := { root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray }, congrThmCounter := { root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray }, thmsWithBadKeys := { root := PersistentArrayNode.node (Array.mkEmpty PersistentArray.branching.toNat), tail := Array.mkEmpty PersistentArray.branching.toNat, size := 0, shift := PersistentArray.initShift, tailOff := 0 } } }) : MetaM (Option (Array FVarId × MVarId) × Simp.Stats)

Equations

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

def Lean.Meta.simpTargetStar (mvarId : MVarId) (ctx : Simp.Context) (simprocs : Simp.SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none) (stats : Simp.Stats := { usedTheorems := { map := { root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray }, size := 0 }, diag := { usedThmCounter := { root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray }, triedThmCounter := { root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray }, congrThmCounter := { root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray }, thmsWithBadKeys := { root := PersistentArrayNode.node (Array.mkEmpty PersistentArray.branching.toNat), tail := Array.mkEmpty PersistentArray.branching.toNat, size := 0, shift := PersistentArray.initShift, tailOff := 0 } } }) : MetaM (TacticResultCNM × Simp.Stats)

Equations

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

def Lean.Meta.dsimpGoal (mvarId : MVarId) (ctx : Simp.Context) (simprocs : Simp.SimprocsArray := #[]) (simplifyTarget : Bool := true) (fvarIdsToSimp : Array FVarId := #[]) (stats : Simp.Stats := { usedTheorems := { map := { root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray }, size := 0 }, diag := { usedThmCounter := { root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray }, triedThmCounter := { root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray }, congrThmCounter := { root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray }, thmsWithBadKeys := { root := PersistentArrayNode.node (Array.mkEmpty PersistentArray.branching.toNat), tail := Array.mkEmpty PersistentArray.branching.toNat, size := 0, shift := PersistentArray.initShift, tailOff := 0 } } }) : MetaM (Option MVarId × Simp.Stats)

Equations

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