Stream: Coq users

Topic: Meaning of Inline(<number>) in a module


view this post on Zulip Pierre Rousselin (Nov 03 2023 at 06:30):

What does Inline followed by a number means in a module, e.g. (from Coq.Numbers.NatInt.NZAxioms.v) in :

Module Type ZeroSuccPred (Import T:Typ).
 Parameter Inline(20) zero : t.
 Parameter Inline(50) succ : t -> t.
 Parameter Inline pred : t -> t.
End ZeroSuccPred.

view this post on Zulip Gaëtan Gilbert (Nov 03 2023 at 08:31):

I think the main doc for this is currently in an old changelog :(

- 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 Gaëtan Gilbert (Nov 03 2023 at 08:32):

and from fa9175c646ac804af0f446eeb981b2143d310537

  For instance, in ZBinary, eq is @Logic.eq and should rather be inlined,
  while in BigZ, eq is (fun x y => [x]=[y]) and should rather not be inlined.
  We could achieve this behavior by setting a level such as 30 to the
  parameter eq, and then tweaking the current level when applying functors.

view this post on Zulip Pierre Rousselin (Nov 03 2023 at 08:38):

Thank you very much, I will try to understand it and patch the refman.

view this post on Zulip Pierre Rousselin (Nov 03 2023 at 16:12):

I like the "(DOC TODO)" annotation at the end :)


Last updated: Jun 13 2024 at 19:02 UTC