opaque Lean.Meta.Simp.backward.dsimp.proofs : Lean.Option Bool

opaque Lean.Meta.Simp.congrHypothesisExceptionId : InternalExceptionId

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

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

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.

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.

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.

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

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

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

instance Lean.Meta.Simp.instReprSimpLetCase : Repr SimpLetCase

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

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

We use withNewlemmas whenever updating the local context.

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

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

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

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

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

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

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

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

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

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

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

Try to rewrite e children using the given congruence theorem

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

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

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.

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

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

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

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

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

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

@[inline]

def Lean.Meta.Simp.withCatchingRuntimeEx {α : Type} (x : SimpM α) : SimpM α

def Lean.Meta.Simp.mainCore (e : Expr) (ctx : Context) (s : State := { }) (methods : Methods := { }) : MetaM (Result × State)

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

def Lean.Meta.Simp.main (e : Expr) (ctx : Context) (stats : Stats := { }) (methods : Methods := { }) : MetaM (Result × Stats)

def Lean.Meta.Simp.dsimpMainCore (e : Expr) (ctx : Context) (s : State := { }) (methods : Methods := { }) : MetaM (Expr × State)

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

def Lean.Meta.Simp.dsimpMain (e : Expr) (ctx : Context) (stats : Stats := { }) (methods : Methods := { }) : MetaM (Expr × Stats)

def Lean.Meta.simpCore (e : Expr) (ctx : Simp.Context) (simprocs : Simp.SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none) (s : Simp.State := { }) : MetaM (Simp.Result × Simp.State)

def Lean.Meta.simp (e : Expr) (ctx : Simp.Context) (simprocs : Simp.SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none) (stats : Simp.Stats := { }) : MetaM (Simp.Result × Simp.Stats)

def Lean.Meta.dsimp (e : Expr) (ctx : Simp.Context) (simprocs : Simp.SimprocsArray := #[]) (stats : Simp.Stats := { }) : MetaM (Expr × Simp.Stats)

def Lean.Meta.simpTargetCore (mvarId : MVarId) (ctx : Simp.Context) (simprocs : Simp.SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none) (mayCloseGoal : Bool := true) (stats : Simp.Stats := { }) : MetaM (Option MVarId × Simp.Stats)

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

def Lean.Meta.simpTarget (mvarId : MVarId) (ctx : Simp.Context) (simprocs : Simp.SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none) (mayCloseGoal : Bool := true) (stats : Simp.Stats := { }) : 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.

def Lean.Meta.applySimpResult (mvarId : MVarId) (val type : Expr) (r : Simp.Result) (mayCloseGoal : Bool := true) : MetaM (Option (Expr × Expr))

Applies the result r for type (which is inhabited by val). Returns none if the goal was closed. Returns some (val', type') otherwise, where val' : type' and type' is the simplified type.

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

@[deprecated Lean.Meta.applySimpResult (since := "2025-03-26")]

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

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

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 := { }) : 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.

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

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.

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 := { }) : MetaM (Option (FVarId × MVarId) × Simp.Stats)

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 := { }) : MetaM (Option (Array FVarId × MVarId) × Simp.Stats)

def Lean.Meta.simpTargetStar (mvarId : MVarId) (ctx : Simp.Context) (simprocs : Simp.SimprocsArray := #[]) (discharge? : Option Simp.Discharge := none) (stats : Simp.Stats := { }) : MetaM (TacticResultCNM × Simp.Stats)

def Lean.Meta.dsimpGoal (mvarId : MVarId) (ctx : Simp.Context) (simprocs : Simp.SimprocsArray := #[]) (simplifyTarget : Bool := true) (fvarIdsToSimp : Array FVarId := #[]) (stats : Simp.Stats := { }) : MetaM (Option MVarId × Simp.Stats)