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

opaque Lean.Meta.Simp.debug.simp.check.have : 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.

@[implicit_reducible]

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

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

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

We use withNewLemmas whenever updating the local context.

@[implicit_reducible]

instance Lean.Meta.Simp.instMonadSimpSimpM : MonadSimp SimpM

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.simpHaveTelescope (e : Expr) : SimpM Result

Adapter for Meta.simpHaveTelescope

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

Routine for simplifying let expressions.

If it is a have, we use simpHaveTelescope to simplify entire telescopes at once, to avoid quadratic behavior arising from locally nameless expression representations.

We assume that dependent lets are dependent, but if Config.letToHave is enabled then we attempt to transform it into a have. If that does not change it, then it is only dsimped.

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.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

@[export lean_simp]

def Lean.Meta.Simp.simpImpl (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.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.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.

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)