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
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.
Just replace the projection syntax by the function call syntax:
That works, but that notation is used throughout the project. Is the projection syntax deprecated/reserved for records?
Yes; it is reserved for record projections.
towokit928 has marked this topic as resolved.
Last updated: Oct 03 2023 at 20:01 UTC