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

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

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.

def Lean.Meta.Simp.Result.getProof (r : Lean.Meta.Simp.Result) : Lean.MetaM Lean.Expr

def Lean.Meta.Simp.Result.getProof' (source : Lean.Expr) (r : Lean.Meta.Simp.Result) : Lean.MetaM Lean.Expr

Similar to Result.getProof, but adds a mkExpectedTypeHint if proof? is none (i.e., result is definitionally equal to input), but we cannot establish that source and r.expr are definitionally when using TransparencyMode.reducible.

def Lean.Meta.Simp.mkCongrFun (r : Lean.Meta.Simp.Result) (a : Lean.Expr) : Lean.MetaM Lean.Meta.Simp.Result

def Lean.Meta.Simp.mkCongr (r₁ : Lean.Meta.Simp.Result) (r₂ : Lean.Meta.Simp.Result) : Lean.MetaM Lean.Meta.Simp.Result

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

instance Lean.Meta.Simp.instInhabitedM {α : Type} : Inhabited (Lean.Meta.Simp.M α)

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

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

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

def Lean.Meta.Simp.removeUnnecessaryCasts (e : Lean.Expr) : Lean.MetaM Lean.Expr

Given the application e, remove unnecessary casts of the form Eq.rec a rfl and Eq.ndrec a rfl.

def Lean.Meta.Simp.removeUnnecessaryCasts.isDummyEqRec (e : Lean.Expr) : Bool

partial def Lean.Meta.Simp.removeUnnecessaryCasts.elimDummyEqRec (e : Lean.Expr) : Lean.Expr

partial def Lean.Meta.Simp.simp (e : Lean.Expr) : Lean.Meta.Simp.M Lean.Meta.Simp.Result

partial def Lean.Meta.Simp.simp.simpLoop (e : Lean.Expr) (r : Lean.Meta.Simp.Result) : Lean.Meta.Simp.M Lean.Meta.Simp.Result

partial def Lean.Meta.Simp.simp.simpStep (e : Lean.Expr) : Lean.Meta.Simp.M Lean.Meta.Simp.Result

def Lean.Meta.Simp.simp.simpLit (e : Lean.Expr) : Lean.Meta.Simp.M Lean.Meta.Simp.Result

partial def Lean.Meta.Simp.simp.simpProj (e : Lean.Expr) : Lean.Meta.Simp.M Lean.Meta.Simp.Result

partial def Lean.Meta.Simp.simp.congrArgs (r : Lean.Meta.Simp.Result) (args : Array Lean.Expr) : Lean.Meta.Simp.M Lean.Meta.Simp.Result

partial def Lean.Meta.Simp.simp.visitFn (e : Lean.Expr) : Lean.Meta.Simp.M Lean.Meta.Simp.Result

def Lean.Meta.Simp.simp.mkCongrSimp? (f : Lean.Expr) : Lean.Meta.Simp.M (Option Lean.Meta.CongrTheorem)

partial def Lean.Meta.Simp.simp.tryAutoCongrTheorem? (e : Lean.Expr) : Lean.Meta.Simp.M (Option Lean.Meta.Simp.Result)

Try to use automatically generated congruence theorems. See mkCongrSimp?.

partial def Lean.Meta.Simp.simp.congrDefault (e : Lean.Expr) : Lean.Meta.Simp.M Lean.Meta.Simp.Result

partial def Lean.Meta.Simp.simp.processCongrHypothesis (h : Lean.Expr) : Lean.Meta.Simp.M Bool

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

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

Try to rewrite e children using the given congruence theorem

partial def Lean.Meta.Simp.simp.congr (e : Lean.Expr) : Lean.Meta.Simp.M Lean.Meta.Simp.Result

partial def Lean.Meta.Simp.simp.simpApp (e : Lean.Expr) : Lean.Meta.Simp.M Lean.Meta.Simp.Result

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

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

partial def Lean.Meta.Simp.simp.simpLambda (e : Lean.Expr) : Lean.Meta.Simp.M Lean.Meta.Simp.Result

partial def Lean.Meta.Simp.simp.simpArrow (e : Lean.Expr) : Lean.Meta.Simp.M Lean.Meta.Simp.Result

partial def Lean.Meta.Simp.simp.simpForall (e : Lean.Expr) : Lean.Meta.Simp.M Lean.Meta.Simp.Result

partial def Lean.Meta.Simp.simp.simpLet (e : Lean.Expr) : Lean.Meta.Simp.M Lean.Meta.Simp.Result

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

@[inline]

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

def Lean.Meta.Simp.main (e : Lean.Expr) (ctx : Lean.Meta.Simp.Context) (usedSimps : optParam Lean.Meta.Simp.UsedSimps ∅) (methods : optParam Lean.Meta.Simp.Methods { pre := fun e => pure (Lean.Meta.Simp.Step.visit { expr := e, proof? := none, dischargeDepth := 0 }), post := fun e => pure (Lean.Meta.Simp.Step.done { expr := e, proof? := none, dischargeDepth := 0 }), discharge? := fun x => pure none }) : Lean.MetaM (Lean.Meta.Simp.Result × Lean.Meta.Simp.UsedSimps)

def Lean.Meta.Simp.dsimpMain (e : Lean.Expr) (ctx : Lean.Meta.Simp.Context) (usedSimps : optParam Lean.Meta.Simp.UsedSimps ∅) (methods : optParam Lean.Meta.Simp.Methods { pre := fun e => pure (Lean.Meta.Simp.Step.visit { expr := e, proof? := none, dischargeDepth := 0 }), post := fun e => pure (Lean.Meta.Simp.Step.done { expr := e, proof? := none, dischargeDepth := 0 }), discharge? := fun x => pure none }) : Lean.MetaM (Lean.Expr × Lean.Meta.Simp.UsedSimps)

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

Return true if e is of the form (x : α) → ... → s = t → ... → False

Recall that this kind of proposition is generated by Lean when creating equations for functions and match-expressions with overlapping cases. Example: the following match-expression has overlapping cases.

def f (x y : Nat) :=
  match x, y with
  | Nat.succ n, Nat.succ m => ...
  | _, _ => 0

The second equation is of the form

(x y : Nat) → ((n m : Nat) → x = Nat.succ n → y = Nat.succ m → False) → f x y = 0

The hypothesis (n m : Nat) → x = Nat.succ n → y = Nat.succ m → False is essentially saying the first case is not applicable.

partial def Lean.Meta.Simp.isEqnThmHypothesis.go (e : Lean.Expr) : Bool

@[inline, reducible]

abbrev Lean.Meta.Simp.Discharge : Type

def Lean.Meta.Simp.dischargeUsingAssumption? (e : Lean.Expr) : Lean.Meta.SimpM (Option Lean.Expr)

def Lean.Meta.Simp.dischargeEqnThmHypothesis? (e : Lean.Expr) : Lean.MetaM (Option Lean.Expr)

Tries to solve e using unifyEq?. It assumes that isEqnThmHypothesis e is true.

partial def Lean.Meta.Simp.dischargeEqnThmHypothesis?.go? (mvarId : Lean.MVarId) : Lean.MetaM (Option Lean.MVarId)

partial def Lean.Meta.Simp.DefaultMethods.discharge? (e : Lean.Expr) : Lean.Meta.SimpM (Option Lean.Expr)

partial def Lean.Meta.Simp.DefaultMethods.pre (e : Lean.Expr) : Lean.Meta.SimpM Lean.Meta.Simp.Step

partial def Lean.Meta.Simp.DefaultMethods.post (e : Lean.Expr) : Lean.Meta.SimpM Lean.Meta.Simp.Step

def Lean.Meta.Simp.DefaultMethods.methods : Lean.Meta.Simp.Methods

def Lean.Meta.simp (e : Lean.Expr) (ctx : Lean.Meta.Simp.Context) (discharge? : optParam (Option Lean.Meta.Simp.Discharge) none) (usedSimps : optParam Lean.Meta.Simp.UsedSimps ∅) : Lean.MetaM (Lean.Meta.Simp.Result × Lean.Meta.Simp.UsedSimps)

def Lean.Meta.dsimp (e : Lean.Expr) (ctx : Lean.Meta.Simp.Context) (usedSimps : optParam Lean.Meta.Simp.UsedSimps ∅) : Lean.MetaM (Lean.Expr × Lean.Meta.Simp.UsedSimps)

def Lean.Meta.applySimpResultToTarget (mvarId : Lean.MVarId) (target : Lean.Expr) (r : Lean.Meta.Simp.Result) : Lean.MetaM Lean.MVarId

Auxiliary method. Given the current target of mvarId, apply r which is a new target and proof that it is equal to the current one.

def Lean.Meta.simpTargetCore (mvarId : Lean.MVarId) (ctx : Lean.Meta.Simp.Context) (discharge? : optParam (Option Lean.Meta.Simp.Discharge) none) (mayCloseGoal : optParam Bool true) (usedSimps : optParam Lean.Meta.Simp.UsedSimps ∅) : Lean.MetaM (Option Lean.MVarId × Lean.Meta.Simp.UsedSimps)

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

def Lean.Meta.simpTarget (mvarId : Lean.MVarId) (ctx : Lean.Meta.Simp.Context) (discharge? : optParam (Option Lean.Meta.Simp.Discharge) none) (mayCloseGoal : optParam Bool true) (usedSimps : optParam Lean.Meta.Simp.UsedSimps ∅) : Lean.MetaM (Option Lean.MVarId × Lean.Meta.Simp.UsedSimps)

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

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

def Lean.Meta.simpStep (mvarId : Lean.MVarId) (proof : Lean.Expr) (prop : Lean.Expr) (ctx : Lean.Meta.Simp.Context) (discharge? : optParam (Option Lean.Meta.Simp.Discharge) none) (mayCloseGoal : optParam Bool true) (usedSimps : optParam Lean.Meta.Simp.UsedSimps ∅) : Lean.MetaM (Option (Lean.Expr × Lean.Expr) × Lean.Meta.Simp.UsedSimps)

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 : Lean.MVarId) (fvarId : Lean.FVarId) (r : Option (Lean.Expr × Lean.Expr)) : Lean.MetaM (Option (Lean.FVarId × Lean.MVarId))

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.

def Lean.Meta.simpLocalDecl (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) (ctx : Lean.Meta.Simp.Context) (discharge? : optParam (Option Lean.Meta.Simp.Discharge) none) (mayCloseGoal : optParam Bool true) (usedSimps : optParam Lean.Meta.Simp.UsedSimps ∅) : Lean.MetaM (Option (Lean.FVarId × Lean.MVarId) × Lean.Meta.Simp.UsedSimps)

def Lean.Meta.simpGoal (mvarId : Lean.MVarId) (ctx : Lean.Meta.Simp.Context) (discharge? : optParam (Option Lean.Meta.Simp.Discharge) none) (simplifyTarget : optParam Bool true) (fvarIdsToSimp : optParam (Array Lean.FVarId) #[]) (usedSimps : optParam Lean.Meta.Simp.UsedSimps ∅) : Lean.MetaM (Option (Array Lean.FVarId × Lean.MVarId) × Lean.Meta.Simp.UsedSimps)

def Lean.Meta.simpTargetStar (mvarId : Lean.MVarId) (ctx : Lean.Meta.Simp.Context) (discharge? : optParam (Option Lean.Meta.Simp.Discharge) none) (usedSimps : optParam Lean.Meta.Simp.UsedSimps ∅) : Lean.MetaM (Lean.Meta.TacticResultCNM × Lean.Meta.Simp.UsedSimps)

def Lean.Meta.dsimpGoal (mvarId : Lean.MVarId) (ctx : Lean.Meta.Simp.Context) (simplifyTarget : optParam Bool true) (fvarIdsToSimp : optParam (Array Lean.FVarId) #[]) (usedSimps : optParam Lean.Meta.Simp.UsedSimps ∅) : Lean.MetaM (Option Lean.MVarId × Lean.Meta.Simp.UsedSimps)