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 : Lean.Meta.Simp.DischargeResult.toCtorIdx x = Lean.Meta.Simp.DischargeResult.toCtorIdx y then isTrue ⋯ else isFalse ⋯

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

Wrapper for invoking discharge?. 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 : Lean.Expr) (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?.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

def Lean.Meta.Simp.simpCtorEq : Lean.Meta.Simp.Simproc

Equations

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

@[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 : Lake.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 : optParam 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 : optParam Bool false) : Lean.Meta.Simp.Simproc

Equations

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

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 = HAndThen.hAndThen Lean.Meta.Simp.rewritePre fun (x : Unit) => HAndThen.hAndThen Lean.Meta.Simp.simpMatch fun (x : Unit) => Lean.Meta.Simp.userPreSimprocs s

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

Equations

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

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

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

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

Equations

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

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 = (Lean.Expr.isForall e && Lean.Meta.Simp.isEqnThmHypothesis.go e)

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

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

Equations

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

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.dischargeDefault? (e : Lean.Expr) : Lean.Meta.SimpM (Option Lean.Expr)

Equations

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

@[inline, reducible]

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) : Lean.Meta.Simp.Methods

Equations

• Lean.Meta.Simp.mkMethods s discharge? = { pre := Lean.Meta.Simp.preDefault s, post := Lean.Meta.Simp.postDefault s, discharge? := discharge? }

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?

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

Equations

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