-
Notifications
You must be signed in to change notification settings - Fork 25
some work on the doc #175
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
some work on the doc #175
Conversation
| - [StructureName.of T : StructureName sT] infers the class of the canonical [StructureName.type] of [T]. | ||
| - [StructureName.Build T cT : StructureName T] outputs the class of the canonical, | ||
| and [StructureName.type] of [cT], and give it the type [Structure]. So that it is | ||
| ready to use in combination with HB.instance, as in |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
@CohenCyril I've some troubles understanding this lat bullet point, see also the change below
structures.v
Outdated
| (* not sure I get this use case *) | ||
| HB.instance Definition _ := StructureName.Build T cT. | ||
| (* cloning a structure *) | ||
| HB.instance Definition _ := StructureName.Build T' (StructureName.of T). |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
| (* not sure I get this use case *) | |
| HB.instance Definition _ := StructureName.Build T cT. | |
| (* cloning a structure *) | |
| HB.instance Definition _ := StructureName.Build T' (StructureName.of T). | |
| (* cloning a structure *) | |
| HB.instance Definition _ := StructureName.Build T cT. |
I see why you are confused. Build does not have the same type as for factories and mixins.
Indeed we since the only authorized way of making a class is to get it from another structure
StructureName.Build T' (StructureName.of T). would be redundant, that's way I skip StructureName.of altogether and the second argument of StructureName.Build is simply another structure we want to take the class from.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Maybe it should have another name. Maybe we should even redefine clone to be this one...
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I liked the fact that it's a Build because T comes first and then "how to build" is simply different by nature for classes.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The example does not show how you get cT, so I'm not so sure I can fix the comment myself.
It is not just the code snippet, it is also the bullet point which fails to parse to me.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
- [StructureName.Build T cT : StructureName T] outputs the class of the canonical,
and [StructureName.type] of [cT], and give it the type [Structure]. So that it is
ready to use in combination with HB.instance, as in
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
S.Build T cT builds a class record. It is projected out the canonical S on T. [Structure] seem unbound.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It should read:
- [StructureName.Build T cT] outputs the class of the canonical [StructureName.type] of [cT],
and gives it the type [StructureName T]. So that it is ready to use in combination with HB.instance, as in
|
Can you clarify the naming convention? This is my understanding
but I guess it is wrong |
Right, I should use |
|
Maybe I should have opened an issue instead of a PR, and let you open the PR. |
|
Great! |
No description provided.