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

Improve code documentation, second batch #106

Merged
merged 1 commit into from
Jul 28, 2020
Merged

Conversation

yannham
Copy link
Member

@yannham yannham commented Jul 24, 2020

Follow-up of #105.

//! - *Values*: merging any other values succeeds if and only if these two values are equals, in which case it evaluates to
//! this common value.
//!
//! Note that merging of lists is not yet implemented.
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I suppose that, on list, merging ought to be “the lists have the same size, and we recursively merge corresponding elements”. Or maybe not, I don't know. Is there a design issue?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Not really, it's just that lists were added after merging and this particular point has not been discussed. I think we can either not give it a special treatment (only merge identical lists), and rely on a future support for user-defined merge to do something different, or implement directly your suggestion.

Comment on lines +36 to +37
//! - *Default/default*: merging two terms with default (either `Default` or `ContractDefault`) fails, as there cannot
//! be two default values for the same field
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Shouldn't it be the merge of both default values, really?

Copy link
Member Author

@yannham yannham Jul 28, 2020

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, probably. Let me make an issue and fix it in another PR.

src/merge.rs Outdated Show resolved Hide resolved
src/operation.rs Outdated Show resolved Hide resolved
src/operation.rs Outdated Show resolved Hide resolved
src/position.rs Show resolved Hide resolved
@yannham yannham merged commit 798d5ea into master Jul 28, 2020
@yannham yannham deleted the doc/improve-code-doc-2 branch July 28, 2020 13:49
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 this pull request may close these issues.

2 participants