def Lean.Meta.Linear.parentIsTarget (parent? : Option Lean.Expr) : Bool

Equations

• Lean.Meta.Linear.parentIsTarget none = false
• Lean.Meta.Linear.parentIsTarget (some parent) = (Lean.Meta.Linear.isLinearTerm parent || Lean.Meta.Linear.isLinearCnstr parent)

def Lean.Meta.Linear.simp? (e : Lean.Expr) (parent? : Option Lean.Expr) : Lean.MetaM (Option (Lean.Expr × Lean.Expr))

Equations

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