Stream: Coq users

Topic: Module System


view this post on Zulip Yannick Zakowski (May 14 2020 at 21:39):

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?

view this post on Zulip Yannick Zakowski (May 14 2020 at 21:40):

I'm also kinda unsure what functor application means for modules without arguments. It is then at definition time?

view this post on Zulip Matthieu Sozeau (May 15 2020 at 09:40):

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).

view this post on Zulip Yannick Zakowski (May 15 2020 at 13:13):

Ah should have checked the change logs indeed, thanks Matthieu!

view this post on Zulip Enrico Tassi (May 15 2020 at 13:39):

Is it a released changelog? (it says "DOC TODO")

view this post on Zulip Enrico Tassi (May 15 2020 at 13:39):

Maybe we should open an issue?

view this post on Zulip Théo Zimmermann (May 15 2020 at 13:40):

There are 6 occurrences of "DOC TODO" in the released changelog.

view this post on Zulip Théo Zimmermann (May 15 2020 at 13:41):

All of them from 8.4beta

view this post on Zulip Théo Zimmermann (May 15 2020 at 13:41):

That's definitely worth opening an issue.

view this post on Zulip Enrico Tassi (May 15 2020 at 13:54):

ISSUE TODO :grinning_face_with_smiling_eyes:

view this post on Zulip Enrico Tassi (May 15 2020 at 13:55):

https://github.com/coq/coq/issues/12333

view this post on Zulip Enrico Tassi (May 15 2020 at 13:55):

We are getting close to 12345, we should make a contest


Last updated: Jan 27 2023 at 01:03 UTC