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:
https://github.com/coq/coq/issues/12333
We are getting close to 12345, we should make a contest
Last updated: Oct 13 2024 at 01:02 UTC