fixes #1176 (duplicate in doc)#1180
Conversation
affeldt-aist
added
the
documentation 📝
| (* Content_SubSigmaAdditive_isMeasure == mixin that extends a content to *) | ||
| (* a measure with the proof that it is *) | ||
| (* semi_sigma_additive *) | ||
| (* Content_isMeasure == mixin that extends a content to a measure *) |
There was a problem hiding this comment.
Well technically, mixins are factories, and the doc probably shouldn't care to document which factories are mixin or not (because the user shouldn't rely on that and doe not need to know it).
There was a problem hiding this comment.
Should we call them all "interfaces"? "factory" is a bit HB-specific. "mixin" is not HB-specific but calling "mixins" "factories" might not help.
There was a problem hiding this comment.
At least factory is what it is called in the (the bit of) doc we have for HB. Not sure it would be easy to relate a new term like "interface" to that. And at least, factory conveys well the fact that the thing is used to build an instance of the structure. "interface" seems to vague to me.
| (* The HB class is SFiniteMeasure. *) | ||
| (* sfinite_measure_seq mu == the sequence of finite measures of the *) | ||
| (* s-finite measure mu *) | ||
| (* Measure_isSFinite_subdef == mixin for s-finite measures *) |
There was a problem hiding this comment.
Maybe this shouldn't be called _subdef if it needs to be documented?
2 participants
Motivation for this change
fixes #1176
It looks like some past merge has messed up with the documentation of
measure.v.It should be fixes now.
FYI: @yoshihiro503, @CohenCyril
Checklist
- [ ] added corresponding entries inCHANGELOG_UNRELEASED.mdReference: How to document
Reminder to reviewers