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!
Julin S has marked this topic as resolved.
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