Proof By Sledgehammer (Oct 15 2021 at 19:37): 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.
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: Oct 13 2024 at 01:02 UTC