Julin S (Dec 02 2022 at 07:54): Julin S (Dec 02 2022 at 07:54):I see that returning the value being matched itself just like that was casuing the problem. Something for me to keep in mind.
And I wasn't aware of the as e' syntax.
Thanks!
Notification Bot (Dec 02 2022 at 07:55):Julin S has marked this topic as resolved.
Meven Lennon-Bertrand (Dec 02 2022 at 10:35):The deeper issue is that if you are in branch, the type of the scrutinee does not change. So here in the branch for Const e still has type exp V t while the type of e' is exp V Nat, which is really what you want. And regarding the as keyword, it can be used to name any part of a branch pattern, not just the top-level one, which can prove handy at times.
Last updated: Feb 06 2023 at 12:04 UTC