Stream: Coq users

Topic: ✔ Use Haskell-like Import syntax

Proof By Sledgehammer (Oct 15 2021 at 19:37):

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.

Gaëtan Gilbert (Oct 15 2021 at 19:38):

the closest you can do is Require Foo. Module F := Foo. Import F. I think

Proof By Sledgehammer (Oct 15 2021 at 19:45):

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?

Proof By Sledgehammer (Oct 15 2021 at 19:50):

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.

Paolo Giarrusso (Oct 15 2021 at 20:23):

So just "Module F := Foo." (after Require)?

Proof By Sledgehammer (Oct 15 2021 at 21:02):

oh, yes. This was much easier than I thought.

Notification Bot (Oct 15 2021 at 21:05):

Daniel Spaniol has marked this topic as resolved.

Last updated: Apr 19 2024 at 15:02 UTC