idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-09-21 10:18:23 +03:00
Code Issues Projects Releases Wiki Activity

Updated documentation for export (#344)

Browse Source 
Co-authored-by: Thomas Herzog <thomas-github@poto.cafe>
This commit is contained in:
TomasPuverle 2020-06-21 12:17:34 -07:00 committed by GitHub
parent d94b86e62c
commit 833a24cb45
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 14 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

15
docs/source/tutorial/modules.rst
View File

@ -117,7 +117,7 @@ Meaning for Functions
about doing this.
.. note::
Type synonyms in Idris are created by writing a function. When
setting the visibility for a module, it is usually a good idea to
``public export`` all type synonyms if they are to be used outside
@ -129,6 +129,19 @@ this effectively makes the function definition part of the module's API.
Therefore, it's generally a good idea to avoid using ``public export`` for
functions unless you really mean to export the full definition.
.. note::
*For beginners*:
If the function needs to be accessed only at runtime, use ``export``.
However, if it's also meant to be used at *compile* time (e.g. to prove
a theorem), use ``public export``.
For example, consider the function ``plus : Nat -> Nat -> Nat`` discussed
previously, and the following theorem: ``thm : plus Z m = m``.
In order to to prove it, the type checker needs to reduce ``plus Z m`` to ``m``
(and hence obtain ``thm : m = m``).
To achieve this, it will need access to the *definition* of ``plus``,
which includes the equation ``plus Z m = m``.
Therefore, in this case, ``plus`` has to be marked as ``public export``.
Meaning for Data Types
----------------------