Stream: Coq users

Topic: ✔ Use Haskell-like Import syntax


view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Oct 15 2021 at 19:38):

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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Oct 15 2021 at 20:23):

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

view this post on Zulip Proof By Sledgehammer (Oct 15 2021 at 21:02):

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

view this post on Zulip Notification Bot (Oct 15 2021 at 21:05):

Daniel Spaniol has marked this topic as resolved.


Last updated: Feb 08 2023 at 22:03 UTC