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

Equations

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

def Lean.Meta.Simp.synthesizeArgs (thmId : Lean.Meta.Origin) (xs : Array Lean.Expr) (bis : Array Lean.BinderInfo) (discharge? : Lean.Expr → Lean.Meta.SimpM (Option 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) (discharge? : Lean.Expr → Lean.Meta.SimpM (Option Lean.Expr)) : 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) (discharge? : Lean.Expr → Lean.Meta.SimpM (Option Lean.Expr)) : 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.getDtConfig (cfg : Lean.Meta.Simp.Config) : Lean.Meta.WhnfCoreConfig

Return a WHNF configuration for retrieving [simp] from the discrimination tree. If user has disabled zeta and/or beta reduction in the simplifier, we must also disable them when retrieving lemmas from discrimination tree. See issues: #2669 and #2281

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

@[inline]

def Lean.Meta.Simp.andThen (s : Lean.Meta.Simp.Step) (f? : Lean.Expr → Lean.Meta.SimpM (Option Lean.Meta.Simp.Step)) : Lean.Meta.SimpM Lean.Meta.Simp.Step

Equations

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

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

Equations

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

@[inline]

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

Equations

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

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

Equations

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

@[inline]

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

Equations

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

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

Equations

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

def Lean.Meta.Simp.simpMatchCore? (app : Lean.Meta.MatcherApp) (e : Lean.Expr) (discharge? : Lean.Expr → Lean.Meta.SimpM (Option Lean.Expr)) : Lean.Meta.SimpM (Option Lean.Meta.Simp.Step)

Equations

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

def Lean.Meta.Simp.simpMatch? (discharge? : Lean.Expr → Lean.Meta.SimpM (Option Lean.Expr)) (e : Lean.Expr) : Lean.Meta.SimpM (Option Lean.Meta.Simp.Step)

Equations

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

def Lean.Meta.Simp.rewritePre (e : Lean.Expr) (discharge? : Lean.Expr → Lean.Meta.SimpM (Option Lean.Expr)) (rflOnly : optParam Bool false) : Lean.Meta.SimpM Lean.Meta.Simp.Step

Equations

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

def Lean.Meta.Simp.rewritePost (e : Lean.Expr) (discharge? : Lean.Expr → Lean.Meta.SimpM (Option Lean.Expr)) (rflOnly : optParam Bool false) : Lean.Meta.SimpM Lean.Meta.Simp.Step

Equations

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

def Lean.Meta.Simp.preDefault (e : Lean.Expr) (discharge? : Lean.Expr → Lean.Meta.SimpM (Option Lean.Expr)) : Lean.Meta.SimpM Lean.Meta.Simp.Step

Equations

• Lean.Meta.Simp.preDefault e discharge? = do let s ← Lean.Meta.Simp.rewritePre e discharge? false Lean.Meta.Simp.andThen s Lean.Meta.Simp.tryRewriteUsingDecide?

def Lean.Meta.Simp.postDefault (e : Lean.Expr) (discharge? : Lean.Expr → Lean.Meta.SimpM (Option Lean.Expr)) : Lean.Meta.SimpM Lean.Meta.Simp.Step

Equations

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