inductive Lean.Meta.Simp.DischargeResult : Type

Helper type for implementing discharge?'

• proved : DischargeResult
• notProved : DischargeResult
• maxDepth : DischargeResult
• failedAssign : DischargeResult

instance Lean.Meta.Simp.instDecidableEqDischargeResult : DecidableEq DischargeResult

def Lean.Meta.Simp.discharge?' (thmId : Origin) (x type : Expr) : 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.

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

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

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

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

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

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

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

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

def Lean.Meta.Simp.rewrite?.rewriteNoIndex? (e : Expr) (s : SimpTheoremTree) (erased : PHashSet Origin) (tag : String) (rflOnly : Bool) : SimpM (Option 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.

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

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

@[inline]

def Lean.Meta.Simp.simpUsingDecide : Simproc

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

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

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

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

def Lean.Meta.Simp.simpMatch : Simproc

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

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

def Lean.Meta.Simp.drewritePre : DSimproc

def Lean.Meta.Simp.drewritePost : DSimproc

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

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

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

Discharge procedure for the ground/symbolic evaluator.

def Lean.Meta.Simp.sevalGround : Simproc

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

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

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

def Lean.Meta.Simp.mkSEvalMethods : CoreM Methods

def Lean.Meta.Simp.mkSEvalContext : MetaM Context

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

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

def Lean.Meta.Simp.simpGround : Simproc

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

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

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

def Lean.Meta.Simp.isEqnThmHypothesis (e : 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 : Expr) : Bool

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

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

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

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

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

@[reducible, inline]

abbrev Lean.Meta.Simp.Discharge : Type

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

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

def Lean.Meta.Simp.mkDefaultMethods : CoreM Methods