[ doc ] Add missing pragmas to documentation #3148
Conversation
docs/source/reference/pragmas.rst
Outdated
| ``%default`` | ||
| -------------------- | ||
|
|
||
| Set the default totality requirement for functions. The initial value is `covering`, which |
There was a problem hiding this comment.
Maybe, it's worth adding that total can be an initial value if an appropriate flag is passed to the compiler
docs/source/reference/pragmas.rst
Outdated
| ``%defaulthint`` | ||
| -------------------- | ||
|
|
||
| Mark a default for functions like ``fromString`` in cases where the compiler cannot |
There was a problem hiding this comment.
This seems to give a wrong to impression. I would say that this is like a %hint which is tried when none of the proper %hints succeeded.
docs/source/reference/pragmas.rst
Outdated
| ``%hint`` | ||
| -------------------- | ||
|
|
||
| Mark a function to be used for ``auto`` search (see :ref:`auto-implicits` for more). |
There was a problem hiding this comment.
Maybe, it's important to add that every non-named implementation receives this pragma automatically. Also, it may be added that every data constructor effectively receives this unless [noHints] is present in the declaration of the data type.
docs/source/reference/pragmas.rst
Outdated
| ``%globalhint`` | ||
| -------------------- | ||
|
|
||
| This pragma is similar to ``%defaulthint``. |
There was a problem hiding this comment.
As far as I know, this is similar to %hint, not %defaulthint, but the rules of search are different. %hints have determining type arguments, but %globalhints are tried anyway.
There was a problem hiding this comment.
I see. The %globalhint are stored with the %defaulthint, because neither relies on the type, but they're used very differently. It looks like %globalhint wins over %hint, too.
Thanks for the feedback. I'll try to get an update out tomorrow.
|
Seems like all the feedback has been addressed and it looks good to me. Maybe we can start thinking about removing the deprecated pragmas soon |
Description
This PR adds documentation for all of the pragmas in Idris. It is based off of the list in the comments of #3072.
There are 43 of them, so I broke them into sections:
Let me know if there is a better way to organize them.
It still needs some clarification on how
%globalhintdiffers from%defaulthint. I copied the description for%syntacticfrom a comment in the source code, but I don't fully understand what it does.I found that
%allow_overloadsis no longer used and documented that. It updates the configuration, but nothing reads that data. It was disabled here:Idris2/src/TTImp/Elab/Ambiguity.idr
Lines 294 to 298 in d6aa70d
We don't seem to have any documentation on elab reflection in
docs. It'd be nice to add that someday.At some point,
libraries.rstshould be rewritten or removed. It currently references a deprecated pragma, and the first two examples now give errors.Should this change go in the CHANGELOG?
No, it's just updates to documentation.