Lean4
/-- Run each registered `positivity` extension on an expression, returning a `NormNum.Result`. -/
def core (e : Q($α)) : MetaM (Strictness zα pα e) := do
let mut result := .none
trace[Tactic.positivity]"trying to prove positivity of {e}"
for ext in ← (positivityExt.getState (← getEnv)).2.getMatch e do
try
result ← orElse result <| ext.eval zα pα e
catch err =>
trace[Tactic.positivity]"{e } failed: {err.toMessageData}"
result ← orElse result <| normNumPositivity zα pα e
result ← orElse result <| positivityCanon zα pα e
if let .positive _ := result then
trace[Tactic.positivity]"{e } => {result.toString}"
return result
for ldecl in ← getLCtx do
if !ldecl.isImplementationDetail then
result ← orElse result <| compareHyp zα pα e ldecl
trace[Tactic.positivity]"{e } => {result.toString}"
throwNone (pure result)
