Zulip Chat Archive
Stream: mathlib4
Topic: Order.Bounded mathlib4#1042
Moritz Doll (Dec 15 2022 at 21:04):
There are two convert that I don't know how to fix and if someone wants to try, you are very welcome.
Ruben Van de Velde (Dec 15 2022 at 21:22):
Got a fix I'll push in a minute
Ruben Van de Velde (Dec 15 2022 at 21:24):
It turns out lean4 can't figure out what the s argument should be
Last updated: Dec 20 2023 at 11:08 UTC