Stream: Coq users

Topic: Can I create alias when importing

view this post on Zulip Daniel Hilst Selli (Jan 20 2022 at 12:45):

I already have a String module imported and want import Coq.Strings.String as CoqsString I was thinking about something like Require Coq.Strings.String as CoqString but obviously this is not valid

view this post on Zulip Guillaume Melquiond (Jan 20 2022 at 12:46):

You can do Require Coq.Strings.String. Module CoqString = Coq.Strings.String.

view this post on Zulip Daniel Hilst Selli (Jan 20 2022 at 12:50):

Oh that's it, I was trying something like Module CoqString. Require Export Coq.Strings.String. End CoqString

Thank you Guillaume!

Last updated: Sep 26 2023 at 12:02 UTC