The standard library has "Inline" annotations parameters by a number: for instance in the definition of [Typ],
Parameter Inline(10) t : Type.
I do not find in the doc what this number corresponds to, the only doc for inline that I find states the following:
Commandassumption_keyword Inline assums The instance of this assumption will be automatically expanded at functor application, except when this functor application is prefixed by a ! annotation.
Would anyone knows what it corresponds to?
I'm also kinda unsure what functor application means for modules without arguments. It is then at definition time?
Quoting from the changes.rst file:
- The inlining done during application of functors can now be controlled more precisely, by the annotations (no inline) or (inline at level XX). With the latter annotation, only functor parameters whose levels are lower or equal than XX will be inlined. The level of a parameter can be fixed by "Parameter Inline(30) foo". When levels aren't given, the default value is 100. One can also use the flag "Set Inline Level ..." to set a level (DOC TODO).
Ah should have checked the change logs indeed, thanks Matthieu!
Is it a released changelog? (it says "DOC TODO")
Maybe we should open an issue?
There are 6 occurrences of "DOC TODO" in the released changelog.
All of them from 8.4beta
That's definitely worth opening an issue.
ISSUE TODO :grinning_face_with_smiling_eyes:
We are getting close to 12345, we should make a contest
Last updated: Jan 27 2023 at 01:03 UTC