Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

merge precondition message: Constructor alias #4981

Closed
Tracked by #4928
aryairani opened this issue May 20, 2024 · 0 comments · Fixed by #5032
Closed
Tracked by #4928

merge precondition message: Constructor alias #4981

aryairani opened this issue May 20, 2024 · 0 comments · Fixed by #5032

Comments

@aryairani
Copy link
Contributor

aryairani commented May 20, 2024

Constructor alias

Each naming of a decl may not have more than one name for each constructor, within the decl's namespace.

Alice's branch:

unique type Foo = Bar
project/alice> alias.term Foo.Bar Foo.some.other.Alias

  Done.

Bob's branch:

bob : Nat
bob = 100
project/alice> merge /bob

  On project/alice, Foo.Bar and Foo.some.other.Alias are
  aliases. Every type declaration must have exactly one name for
  each constructor.


Maybe something like:

Sorry, I wasn't able to perform the merge:

On project/alice, the Foo type has some constructors with multiple names, and I can't yet perform a merge in this situation:

Foo.Bar
Foo.some.other.Alias

Foo.Baz
Foo.some.other.other.Alias

Please delete all but one name for each constructor, and then try merging again.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging a pull request may close this issue.

1 participant