Stream: math-comp users

Topic: ✔ why guard does not complain?

view this post on Zulip Andrey Klaus (Apr 27 2023 at 20:54):

@Pierre Roux , thank you! I took a look on Nat.sub. Now it is a little bit cleaner for me, I will try to change my code to be similar to Nat.sub.

view this post on Zulip Notification Bot (Apr 27 2023 at 20:54):

Andrey Klaus has marked this topic as resolved.

view this post on Zulip Pierre Roux (Apr 27 2023 at 21:07):

Note that in Nat.sub you'll find things like match n with 0 => n and not match n with 0 => 0 which wouldn't work.

Last updated: Jul 23 2024 at 20:01 UTC