Stream: Coq users

Topic: Print Namespace


view this post on Zulip Pierre Rousselin (Nov 09 2023 at 16:55):

What does Print Namespace dirpath do and what are its limitations?
There is no documentation in the reference manual.
I have tried :

From Coq Require Import Arith.PeanoNat.
Module A.
  Definition N := nat.
End A.
Print Namespace Nat. (* Nat: *)
Print Namespace Coq.Arith.PeanoNat.Nat. (* everything in PeanoNat.Nat *)
Print Namespace A. (* A: *)

So it seems it needs a fully qualified module name?
What about this file's module A?

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

it seems to want a prefix not a suffix

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

so eg Print Namespace Coq -> loads of stuff
Print Namespace current.file.modname -> stuff from the current file


Last updated: Jun 22 2024 at 16:02 UTC