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

Equations

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

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.

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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.

Equations

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

@[inline]

def Lean.Meta.Simp.simpUsingDecide : Simproc

Equations

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

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

Equations

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

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.

Equations

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

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

Equations

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

def Lean.Meta.Simp.simpMatch : Simproc

Equations

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

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

Equations

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

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

Equations

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

def Lean.Meta.Simp.drewritePre : DSimproc

Equations

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

def Lean.Meta.Simp.drewritePost : DSimproc

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def Lean.Meta.Simp.mkSEvalContext : MetaM Context

Equations

• Lean.Meta.Simp.mkSEvalContext = do let s ← liftM Lean.Meta.getSEvalTheorems let c ← liftM Lean.Meta.getSimpCongrTheorems Lean.Meta.Simp.mkContext { ground := true } #[s] c

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

def Lean.Meta.Simp.dischargeEqnThmHypothesis? (e : Expr) : MetaM (Option 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.

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 instantiate 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 : Expr) : SimpM (Option 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 : SimprocsArray) (discharge? : Discharge) (wellBehavedDischarge : Bool) : Methods

Equations

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

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

Equations

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

def Lean.Meta.Simp.mkDefaultMethods : CoreM Methods

Equations

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