Enzo Crance (Nov 19 2022 at 16:39): Enzo Crance (Nov 19 2022 at 16:39):Hello.
Is there a local version of coq.locate? The documentation states that it looks for a global reference.
I would like to open a module, declare a record, and access its fields in subsequent declarations. When running coq.locate on the name of the field (which is supposed to be a function declared right after the inductive that stands for the record), I get nothing, as if the field projector did not exist.
Enrico Tassi (Nov 19 2022 at 20:23):that is weird, it should work. open an issue please
Last updated: Oct 13 2024 at 01:02 UTC