positivity fails

Stream: metaprogramming / tactics

[Yaël Dillies]

Just encountered

import data.real.ennreal

open_locale ennreal

example : (0 : ℝ≥0∞) < 2 := by positivity

Not sure how to fix it, because I suspect this failure traces back to norm_num.

[Alex J. Best]

fwiw this works

import tactic
import data.real.ennreal

open_locale ennreal
example : (0 : ℝ≥0∞) < 2 := by norm_num