inductive Lean.Meta.Simp.DischargeResult : Type

Helper type for implementing discharge?'

• proved: Lean.Meta.Simp.DischargeResult
• notProved: Lean.Meta.Simp.DischargeResult
• maxDepth: Lean.Meta.Simp.DischargeResult
• failedAssign: Lean.Meta.Simp.DischargeResult

instance Lean.Meta.Simp.instDecidableEqDischargeResult : DecidableEq Lean.Meta.Simp.DischargeResult

Equations

• Lean.Meta.Simp.instDecidableEqDischargeResult x y = if h : x.toCtorIdx = y.toCtorIdx then isTrue ⋯ else isFalse ⋯

def Lean.Meta.Simp.discharge?' (thmId : Lean.Meta.Origin) (x type : Lean.Expr) : Lean.Meta.SimpM Bool

Wrapper for invoking discharge? method. It checks for maximum discharge depth, create trace nodes, and ensure the generated proof was successfully assigned to x.

Equations

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

def Lean.Meta.Simp.synthesizeArgs (thmId : Lean.Meta.Origin) (bis : Array Lean.BinderInfo) (xs : Array Lean.Expr) : Lean.Meta.SimpM Bool

Equations

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

def Lean.Meta.Simp.synthesizeArgs.synthesizeInstance (thmId : Lean.Meta.Origin) (x type : Lean.Expr) : Lean.Meta.SimpM Bool

Equations

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

def Lean.Meta.Simp.tryTheoremWithExtraArgs? (e : Lean.Expr) (thm : Lean.Meta.SimpTheorem) (numExtraArgs : Nat) : Lean.Meta.SimpM (Option Lean.Meta.Simp.Result)

Equations

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

def Lean.Meta.Simp.tryTheorem? (e : Lean.Expr) (thm : Lean.Meta.SimpTheorem) : Lean.Meta.SimpM (Option Lean.Meta.Simp.Result)

Equations

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

def Lean.Meta.Simp.rewrite? (e : Lean.Expr) (s : Lean.Meta.SimpTheoremTree) (erased : Lean.PHashSet Lean.Meta.Origin) (tag : String) (rflOnly : Bool) : Lean.Meta.SimpM (Option Lean.Meta.Simp.Result)

Remark: the parameter tag is used for creating trace messages. It is irrelevant otherwise.

Equations

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

def Lean.Meta.Simp.rewrite?.rewriteUsingIndex? (e : Lean.Expr) (s : Lean.Meta.SimpTheoremTree) (erased : Lean.PHashSet Lean.Meta.Origin) (tag : String) (rflOnly : Bool) : Lean.Meta.SimpM (Option Lean.Meta.Simp.Result)

For (← getConfig).index := true, use discrimination tree structure when collecting simp theorem candidates.

Equations

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

def Lean.Meta.Simp.rewrite?.rewriteNoIndex? (e : Lean.Expr) (s : Lean.Meta.SimpTheoremTree) (erased : Lean.PHashSet Lean.Meta.Origin) (tag : String) (rflOnly : Bool) : Lean.Meta.SimpM (Option Lean.Meta.Simp.Result)

For (← getConfig).index := false, Lean 3 style simp theorem retrieval. Only the root symbol is taken into account. Most of the structure of the discrimination tree is ignored.

Equations

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

def Lean.Meta.Simp.rewrite?.diagnoseWhenNoIndex (e : Lean.Expr) (s : Lean.Meta.SimpTheoremTree) (thm : Lean.Meta.SimpTheorem) : Lean.Meta.SimpM Unit

Equations

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

def Lean.Meta.Simp.rewrite?.inErasedSet (erased : Lean.PHashSet Lean.Meta.Origin) (thm : Lean.Meta.SimpTheorem) : Bool

Equations

• Lean.Meta.Simp.rewrite?.inErasedSet erased thm = Lean.PersistentHashSet.contains erased thm.origin

@[inline]

def Lean.Meta.Simp.simpUsingDecide : Lean.Meta.Simp.Simproc

Equations

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

def Lean.Meta.Simp.simpArith (e : Lean.Expr) : Lean.Meta.SimpM Lean.Meta.Simp.Step

Equations

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

def Lean.Meta.Simp.simpMatchDiscrs? (info : Lean.Meta.MatcherInfo) (e : Lean.Expr) : Lean.Meta.SimpM (Option Lean.Meta.Simp.Result)

Given a match-application e with MatcherInfo info, return some result if at least of one of the discriminants has been simplified.

Equations

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

def Lean.Meta.Simp.simpMatchCore (matcherName : Lean.Name) (e : Lean.Expr) : Lean.Meta.SimpM Lean.Meta.Simp.Step

Equations

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

def Lean.Meta.Simp.simpMatch : Lean.Meta.Simp.Simproc

Equations

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

def Lean.Meta.Simp.rewritePre (rflOnly : Bool := false) : Lean.Meta.Simp.Simproc

Equations

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

def Lean.Meta.Simp.rewritePost (rflOnly : Bool := false) : Lean.Meta.Simp.Simproc

Equations

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

def Lean.Meta.Simp.drewritePre : Lean.Meta.Simp.DSimproc

Equations

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

def Lean.Meta.Simp.drewritePost : Lean.Meta.Simp.DSimproc

Equations

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

def Lean.Meta.Simp.dpreDefault (s : Lean.Meta.Simp.SimprocsArray) : Lean.Meta.Simp.DSimproc

Equations

• Lean.Meta.Simp.dpreDefault s = Lean.Meta.Simp.drewritePre >> Lean.Meta.Simp.userPreDSimprocs s

def Lean.Meta.Simp.dpostDefault (s : Lean.Meta.Simp.SimprocsArray) : Lean.Meta.Simp.DSimproc

Equations

• Lean.Meta.Simp.dpostDefault s = Lean.Meta.Simp.drewritePost >> Lean.Meta.Simp.userPostDSimprocs s

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

Discharge procedure for the ground/symbolic evaluator.

Equations

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

def Lean.Meta.Simp.sevalGround : Lean.Meta.Simp.Simproc

Try to unfold ground term in the ground/symbolic evaluator.

Equations

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

def Lean.Meta.Simp.preSEval (s : Lean.Meta.Simp.SimprocsArray) : Lean.Meta.Simp.Simproc

Equations

• Lean.Meta.Simp.preSEval s = Lean.Meta.Simp.rewritePre >> Lean.Meta.Simp.simpMatch >> Lean.Meta.Simp.userPreSimprocs s

def Lean.Meta.Simp.postSEval (s : Lean.Meta.Simp.SimprocsArray) : Lean.Meta.Simp.Simproc

Equations

• Lean.Meta.Simp.postSEval s = Lean.Meta.Simp.rewritePost >> Lean.Meta.Simp.userPostSimprocs s >> Lean.Meta.Simp.sevalGround

def Lean.Meta.Simp.mkSEvalMethods : Lean.CoreM Lean.Meta.Simp.Methods

Equations

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

def Lean.Meta.Simp.mkSEvalContext : Lean.CoreM Lean.Meta.Simp.Context

Equations

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

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

Invoke ground/symbolic evaluator from simp. It uses the seval theorems and simprocs.

Equations

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

def Lean.Meta.Simp.simpGround : Lean.Meta.Simp.Simproc

Try to unfold ground term in the ground/symbolic evaluator.

Equations

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

def Lean.Meta.Simp.preDefault (s : Lean.Meta.Simp.SimprocsArray) : Lean.Meta.Simp.Simproc

Equations

• Lean.Meta.Simp.preDefault s = Lean.Meta.Simp.rewritePre >> Lean.Meta.Simp.simpMatch >> Lean.Meta.Simp.userPreSimprocs s >> Lean.Meta.Simp.simpUsingDecide

def Lean.Meta.Simp.postDefault (s : Lean.Meta.Simp.SimprocsArray) : Lean.Meta.Simp.Simproc

Equations

• Lean.Meta.Simp.postDefault s = Lean.Meta.Simp.rewritePost >> Lean.Meta.Simp.userPostSimprocs s >> Lean.Meta.Simp.simpGround >> Lean.Meta.Simp.simpArith >> Lean.Meta.Simp.simpUsingDecide

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.

Equations

• Lean.Meta.Simp.isEqnThmHypothesis e = (e.isForall && Lean.Meta.Simp.isEqnThmHypothesis.go e)

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

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.

Equations

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

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

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

Discharges assumptions of the form ∀ …, a = b using rfl. This is particularly useful for higher order assumptions of the form ∀ …, e = ?g x y to instaniate a parameter g even if that does not appear on the lhs of the rule.

Equations

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

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

Equations

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

@[reducible, inline]

abbrev Lean.Meta.Simp.Discharge : Type

Equations

• Lean.Meta.Simp.Discharge = (Lean.Expr → Lean.Meta.SimpM (Option Lean.Expr))

def Lean.Meta.Simp.mkMethods (s : Lean.Meta.Simp.SimprocsArray) (discharge? : Lean.Meta.Simp.Discharge) (wellBehavedDischarge : Bool) : Lean.Meta.Simp.Methods

Equations

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

def Lean.Meta.Simp.mkDefaultMethodsCore (simprocs : Lean.Meta.Simp.SimprocsArray) : Lean.Meta.Simp.Methods

Equations

• Lean.Meta.Simp.mkDefaultMethodsCore simprocs = Lean.Meta.Simp.mkMethods simprocs Lean.Meta.Simp.dischargeDefault? true

def Lean.Meta.Simp.mkDefaultMethods : Lean.CoreM Lean.Meta.Simp.Methods

Equations

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