Stream: Coq users

Topic: The "Top" logical name


view this post on Zulip Pierre Rousselin (Nov 03 2023 at 09:02):

The refman states (in the Module part):

When Coq is processing a script that hasn't been saved in a file, such as a new buffer in CoqIDE or anything in coqtop, definitions in the script are associated with the logical name Top and there is no associated file system path.

Indeed it works in coqtop. Could it also work in a modified buffer? I'm thinking of Search _ in Top which would be so nice.

view this post on Zulip Paolo Giarrusso (Nov 03 2023 at 13:29):

if the modified buffer was saved, that wouldn't work easily

view this post on Zulip Paolo Giarrusso (Nov 03 2023 at 13:30):

a saved script foo.v can refer to its definitions via its own name foo in some cases, which would break if the name were Top

view this post on Zulip Paolo Giarrusso (Nov 03 2023 at 13:30):

but why not use the real name?

view this post on Zulip Pierre Rousselin (Nov 03 2023 at 16:10):

To be honest here, I'm merely trying to see if this part of the refman is still relevant. But I was also looking for a command to check everything from the top of the current file and I had a tiny hope this could be used.

view this post on Zulip Gaëtan Gilbert (Nov 03 2023 at 17:29):

there's Print All although it doesn't support filtering and doesn't print the content of finished modules


Last updated: Oct 13 2024 at 01:02 UTC