Stream: Coq users

Topic: ✔ A PHOAS example


view this post on Zulip 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!

view this post on Zulip Notification Bot (Dec 02 2022 at 07:55):

Julin S has marked this topic as resolved.

view this post on Zulip 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