Is there a way to Import modules and give them an alternative name like Haskell does with
Import Foo as F?
I would also be happy with just emulating it like
Require Import Foo. Local Notation F := Foo. or something like that.
the closest you can do is
Require Foo. Module F := Foo. Import F. I think
Is there a way to define a shorthand syntax for that? Something like
Notation "'Import' m 'As' n" := (Require m. Module n := m. Import n)? Or do I need to actually hack Coq for that?
Also, this imports the names unqualified, doesn't it? What I would love to have is something like:
(* Foo.v *) Definition Bar := ... (* Other.v *) Import Qualified Foo as F. Check F.Bar. Fail Check Bar.
So just "Module F := Foo." (after Require)?
oh, yes. This was much easier than I thought.
Daniel Spaniol has marked this topic as resolved.
Last updated: Sep 23 2023 at 13:01 UTC