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.
that is weird, it should work. open an issue please
Last updated: Jun 06 2023 at 23:01 UTC