opaque Lean.Meta.Simp.congrHypothesisExceptionId : Lean.InternalExceptionId

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

Equations

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

def Lean.Meta.Simp.Config.updateArith (c : Lean.Meta.Simp.Config) : Lean.CoreM Lean.Meta.Simp.Config

Helper method for bootstrapping purposes. It disables arith if support theorems have not been defined yet.

Equations

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

def Lean.Meta.Simp.isOfNatNatLit (e : Lean.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.isAppOfArity `OfNat.ofNat 3 && e.appFn!.appArg!.isRawNatLit)

def Lean.Meta.Simp.foldRawNatLit (e : Lean.Expr) : Lean.Meta.SimpM Lean.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 : Lean.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 : Lean.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 (Lean.Meta.SimpM α)

Equations

• Lean.Meta.Simp.instInhabitedSimpM = { default := fun (x : Lean.Meta.Simp.MethodsRef) (x : Lean.Meta.Simp.Context) (x : ST.Ref IO.RealWorld Lean.Meta.Simp.State) => default }

def Lean.Meta.Simp.lambdaTelescopeDSimp {α : Type} (e : Lean.Expr) (k : Array Lean.Expr → Lean.Expr → Lean.Meta.SimpM α) : Lean.Meta.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 Lean.Expr → Lean.Expr → Lean.Meta.SimpM α) (xs : Array Lean.Expr) (e : Lean.Expr) : Lean.Meta.SimpM α

inductive Lean.Meta.Simp.SimpLetCase : Type

• dep: Lean.Meta.Simp.SimpLetCase
• nondepDepVar: Lean.Meta.Simp.SimpLetCase
• nondep: Lean.Meta.Simp.SimpLetCase

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

Equations

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

def Lean.Meta.Simp.withNewLemmas {α : Type} (xs : Array Lean.Expr) (f : Lean.Meta.SimpM α) : Lean.Meta.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 : Lean.Expr) : Lean.Meta.SimpM Lean.Meta.Simp.Result

Equations

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

def Lean.Meta.Simp.simpConst (e : Lean.Expr) : Lean.Meta.SimpM Lean.Meta.Simp.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 : Lean.Expr) : Lean.Meta.SimpM Lean.Meta.Simp.Result

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def Lean.Meta.Simp.processCongrHypothesis (h : Lean.Expr) : Lean.Meta.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 : Lean.Meta.SimpCongrTheorem) (e : Lean.Expr) : Lean.Meta.SimpM (Option Lean.Meta.Simp.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 : Lean.Expr) : Lean.Meta.SimpM Lean.Meta.Simp.Result

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

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

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

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

@[export lean_simp]

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

Equations

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

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

Equations

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

@[inline]

def Lean.Meta.Simp.withSimpContext {α : Type} (ctx : Lean.Meta.Simp.Context) (x : Lean.MetaM α) : Lean.MetaM α

Equations

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

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

Equations

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

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

Equations

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

def Lean.Meta.Simp.dsimpMain (e : Lean.Expr) (ctx : Lean.Meta.Simp.Context) (stats : optParam Lean.Meta.Simp.Stats { usedTheorems := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, diag := { usedThmCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, triedThmCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, congrThmCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 } } }) (methods : optParam Lean.Meta.Simp.Methods { pre := fun (x : Lean.Expr) => pure Lean.Meta.Simp.Step.continue, post := fun (e : Lean.Expr) => pure (Lean.Meta.Simp.Step.done { expr := e, proof? := none, cache := true }), dpre := fun (x : Lean.Expr) => pure Lean.TransformStep.continue, dpost := fun (e : Lean.Expr) => pure (Lean.TransformStep.done e), discharge? := fun (x : Lean.Expr) => pure none, wellBehavedDischarge := true }) : Lean.MetaM (Lean.Expr × Lean.Meta.Simp.Stats)

Equations

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

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

Equations

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

def Lean.Meta.simp (e : Lean.Expr) (ctx : Lean.Meta.Simp.Context) (simprocs : optParam Lean.Meta.Simp.SimprocsArray #[]) (discharge? : optParam (Option Lean.Meta.Simp.Discharge) none) (stats : optParam Lean.Meta.Simp.Stats { usedTheorems := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, diag := { usedThmCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, triedThmCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, congrThmCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 } } }) : Lean.MetaM (Lean.Meta.Simp.Result × Lean.Meta.Simp.Stats)

Equations

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

def Lean.Meta.dsimp (e : Lean.Expr) (ctx : Lean.Meta.Simp.Context) (simprocs : optParam Lean.Meta.Simp.SimprocsArray #[]) (stats : optParam Lean.Meta.Simp.Stats { usedTheorems := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, diag := { usedThmCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, triedThmCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, congrThmCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 } } }) : Lean.MetaM (Lean.Expr × Lean.Meta.Simp.Stats)

Equations

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

def Lean.Meta.simpTargetCore (mvarId : Lean.MVarId) (ctx : Lean.Meta.Simp.Context) (simprocs : optParam Lean.Meta.Simp.SimprocsArray #[]) (discharge? : optParam (Option Lean.Meta.Simp.Discharge) none) (mayCloseGoal : optParam Bool true) (stats : optParam Lean.Meta.Simp.Stats { usedTheorems := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, diag := { usedThmCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, triedThmCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, congrThmCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 } } }) : Lean.MetaM (Option Lean.MVarId × Lean.Meta.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 : Lean.MVarId) (ctx : Lean.Meta.Simp.Context) (simprocs : optParam Lean.Meta.Simp.SimprocsArray #[]) (discharge? : optParam (Option Lean.Meta.Simp.Discharge) none) (mayCloseGoal : optParam Bool true) (stats : optParam Lean.Meta.Simp.Stats { usedTheorems := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, diag := { usedThmCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, triedThmCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, congrThmCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 } } }) : Lean.MetaM (Option Lean.MVarId × Lean.Meta.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 : Lean.MVarId) (proof : Lean.Expr) (prop : Lean.Expr) (r : Lean.Meta.Simp.Result) (mayCloseGoal : optParam Bool true) : Lean.MetaM (Option (Lean.Expr × Lean.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 : Lean.MVarId) (fvarId : Lean.FVarId) (r : Lean.Meta.Simp.Result) (mayCloseGoal : Bool) : Lean.MetaM (Option (Lean.Expr × Lean.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 : Lean.MVarId) (proof : Lean.Expr) (prop : Lean.Expr) (ctx : Lean.Meta.Simp.Context) (simprocs : optParam Lean.Meta.Simp.SimprocsArray #[]) (discharge? : optParam (Option Lean.Meta.Simp.Discharge) none) (mayCloseGoal : optParam Bool true) (stats : optParam Lean.Meta.Simp.Stats { usedTheorems := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, diag := { usedThmCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, triedThmCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, congrThmCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 } } }) : Lean.MetaM (Option (Lean.Expr × Lean.Expr) × Lean.Meta.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 : Lean.MVarId) (fvarId : Lean.FVarId) (r : Option (Lean.Expr × Lean.Expr)) : Lean.MetaM (Option (Lean.FVarId × Lean.MVarId))

Equations

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

def Lean.Meta.applySimpResultToLocalDecl (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) (r : Lean.Meta.Simp.Result) (mayCloseGoal : Bool) : Lean.MetaM (Option (Lean.FVarId × Lean.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 : Lean.MVarId) (fvarId : Lean.FVarId) (ctx : Lean.Meta.Simp.Context) (simprocs : optParam Lean.Meta.Simp.SimprocsArray #[]) (discharge? : optParam (Option Lean.Meta.Simp.Discharge) none) (mayCloseGoal : optParam Bool true) (stats : optParam Lean.Meta.Simp.Stats { usedTheorems := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, diag := { usedThmCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, triedThmCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, congrThmCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 } } }) : Lean.MetaM (Option (Lean.FVarId × Lean.MVarId) × Lean.Meta.Simp.Stats)

Equations

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

def Lean.Meta.simpGoal (mvarId : Lean.MVarId) (ctx : Lean.Meta.Simp.Context) (simprocs : optParam Lean.Meta.Simp.SimprocsArray #[]) (discharge? : optParam (Option Lean.Meta.Simp.Discharge) none) (simplifyTarget : optParam Bool true) (fvarIdsToSimp : optParam (Array Lean.FVarId) #[]) (stats : optParam Lean.Meta.Simp.Stats { usedTheorems := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, diag := { usedThmCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, triedThmCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, congrThmCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 } } }) : Lean.MetaM (Option (Array Lean.FVarId × Lean.MVarId) × Lean.Meta.Simp.Stats)

Equations

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

def Lean.Meta.simpTargetStar (mvarId : Lean.MVarId) (ctx : Lean.Meta.Simp.Context) (simprocs : optParam Lean.Meta.Simp.SimprocsArray #[]) (discharge? : optParam (Option Lean.Meta.Simp.Discharge) none) (stats : optParam Lean.Meta.Simp.Stats { usedTheorems := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, diag := { usedThmCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, triedThmCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, congrThmCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 } } }) : Lean.MetaM (Lean.Meta.TacticResultCNM × Lean.Meta.Simp.Stats)

Equations

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

def Lean.Meta.dsimpGoal (mvarId : Lean.MVarId) (ctx : Lean.Meta.Simp.Context) (simprocs : optParam Lean.Meta.Simp.SimprocsArray #[]) (simplifyTarget : optParam Bool true) (fvarIdsToSimp : optParam (Array Lean.FVarId) #[]) (stats : optParam Lean.Meta.Simp.Stats { usedTheorems := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, diag := { usedThmCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, triedThmCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, congrThmCounter := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 } } }) : Lean.MetaM (Option Lean.MVarId × Lean.Meta.Simp.Stats)

Equations

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