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: Missing constructor name #4982

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

merge precondition message: Missing constructor name #4982

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

Comments

@aryairani
Copy link
Contributor

aryairani commented May 20, 2024

Missing constructor name

Each naming of a decl must have a name for each constructor, within the decl's namespace.

Alice's branch:

unique type Foo = Bar
project/alice> delete.term Foo.Bar

  Done.

Bob's branch:

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

  On project/alice, the type Foo is missing a name for one of
  its constructors. Please add one before merging.


Maybe something like:

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

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

You can use view Foo and alias.term <hash> Foo.<ConstructorName> to give names to
each unnamed constructor, and then try the merge 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