Skip to content

Commit

Permalink
[ doc ] updates to hint documentation.
Browse files Browse the repository at this point in the history
  • Loading branch information
dunhamsteve committed Nov 23, 2023
1 parent a03c3bf commit 60ec783
Show file tree
Hide file tree
Showing 2 changed files with 11 additions and 7 deletions.
16 changes: 9 additions & 7 deletions docs/source/reference/pragmas.rst
Original file line number Diff line number Diff line change
Expand Up @@ -29,9 +29,9 @@ Enable language extensions. Currently, the only extension is ``ElabReflection``
``%default``
--------------------

Set the default totality requirement for functions. The initial value is `covering`, which
required case statements to cover, but does not require totality. The other options are
`total` and `partial`.
Set the default totality requirement for functions, which can be one of ``total``,
``covering``, or ``partial``. The value is initially set to ``covering`` unless the ``--total``
command line switch is used, which sets it to ``total``.

``%builtin``
--------------------
Expand Down Expand Up @@ -283,19 +283,21 @@ This pragma is deprecated. Instead use ``%export`` to expose functions to the b
``%hint``
--------------------

Mark a function to be used for ``auto`` search (see :ref:`auto-implicits` for more).
Mark a function to be used for ``auto`` search (see :ref:`auto-implicits` and
:ref:`auto-implicit-arguments` for more). Hints are used internally for instance
resolution and non-named instances are automatically tagged with ``%hint``.


``%defaulthint``
--------------------

Mark a default for functions like ``fromString`` in cases where the compiler cannot
determine which type the user wants.
Mark a hint to be tried when no other hints match.

``%globalhint``
--------------------

This pragma is similar to ``%defaulthint``.
A global hint is like a ``%hint``, but it is always tried, while ``%hint`` is only tried if the return
type matches.

``%extern``
--------------------
Expand Down
2 changes: 2 additions & 0 deletions docs/source/tutorial/miscellany.rst
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,8 @@ omitted when they can be inferred by the type checker [#IdrisType]_, e.g.
index : forall a, n . Fin n -> Vect n a -> a
.. _auto-implicit-arguments:

Auto implicit arguments
-----------------------

Expand Down

0 comments on commit 60ec783

Please sign in to comment.