Zulip Chat Archive

Stream: lean4

Topic: Negation and Floats (Is `Neg.neg` biased towards `Int`?)


view this post on Zulip Andrew Kent (Jan 25 2021 at 20:45):

I just noticed that it's a bit tricky to write down a negated Float value in nested arithmetic expressions. E.g.:

#eval (Neg.neg 42.0)
-- ^ produces the error `failed to synthesize instance OfScientific Int`
-- pointing at `42.0`
#eval (1.0 * -42.0)
-- ^ produces the error `failed to synthesize instance OfScientific Int`
-- pointing again at `42.0`
#eval (1.0 * -(42.0 : Float))
-- ^ works fine

Is there an inference bias towards Int for Neg.neg usages or similar? (I tried to grep for such a bias in the lean4 repo and nothing jumped out at me...)

view this post on Zulip Leonardo de Moura (Jan 25 2021 at 20:50):

Thanks for reporting this issue. I will submit a fix. The issue is due to the priorities of default instances.

view this post on Zulip Leonardo de Moura (Jan 25 2021 at 21:30):

Pushed https://github.com/leanprover/lean4/commit/d408c835d20b6a2f1eee09804222316b755b2ae2


Last updated: May 07 2021 at 11:09 UTC