Stream: Coq users

Topic: ✔ Projections


view this post on Zulip towokit928 (Dec 29 2021 at 07:34):

Hi, I'm trying to compile a Coq project from 2017 with Coq 8.13.2 and am getting this error:

Error: fst is not a projection.

from code like this

st.(fst)

where st is value of a product type created with *.
I see a projection for fst defined here, so I'm not sure why this is happening. How can I allow this code to compile? In the same project, I see the same notation being used for a record defined with Record and it works.

view this post on Zulip Guillaume Melquiond (Dec 29 2021 at 07:41):

Just replace the projection syntax by the function call syntax: fst st.

view this post on Zulip towokit928 (Dec 29 2021 at 08:04):

That works, but that notation is used throughout the project. Is the projection syntax deprecated/reserved for records?

view this post on Zulip Guillaume Melquiond (Dec 29 2021 at 08:21):

Yes; it is reserved for record projections.

view this post on Zulip towokit928 (Dec 29 2021 at 08:37):

Thanks!

view this post on Zulip Notification Bot (Dec 29 2021 at 08:37):

towokit928 has marked this topic as resolved.


Last updated: Feb 01 2023 at 12:30 UTC