Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: positivity fails


Yaël Dillies (Nov 17 2022 at 21:36):

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 (Nov 17 2022 at 21:37):

fwiw this works

import tactic
import data.real.ennreal

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

Last updated: Dec 20 2023 at 11:08 UTC