Zulip Chat Archive
Stream: mathlib4
Topic: calc and isBigO
Yury G. Kudryashov (May 22 2023 at 11:47):
The last bit of !4#4184 that fails to compile is a calc block which fails to synth a Trans instance.
Yury G. Kudryashov (May 22 2023 at 11:47):
While we can comment this example for now, it would be nice to fix it.
Ruben Van de Velde (May 22 2023 at 11:50):
See also !4#4174
Jireh Loreaux (May 24 2023 at 20:26):
@Ruben Van de Velde and @Yury G. Kudryashov , see the changes I just pushed to !4#4174. I wonder if something in the docs4#Trans declaration needs a semiOutParam (@Gabriel Ebner)?
Ruben Van de Velde (May 24 2023 at 20:32):
Oh wow.
Jireh Loreaux (May 24 2023 at 20:34):
FYI: I debugged this by doing a simple abstract example (i.e., with just variables for the functions), which worked. Then I plugged in one-by-one the actual functions in the context until it broke. At that point I tried adding type ascriptions which didn't work, and then I switch to show, which did.
Gabriel Ebner (May 24 2023 at 23:44):
Last updated: Dec 20 2023 at 11:08 UTC