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

Equations

• Lean.Meta.Simp.Arith.parentIsTarget none = false
• Lean.Meta.Simp.Arith.parentIsTarget (some parent) = (Lean.Meta.Simp.Arith.isLinearTerm parent || Lean.Meta.Simp.Arith.isLinearCnstr parent || Lean.Meta.Simp.Arith.isDvdCnstr parent)

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

Equations

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