diff --git a/docs/source/tutorial/modules.rst b/docs/source/tutorial/modules.rst
index 2bc59895d..d635f9da0 100644
--- a/docs/source/tutorial/modules.rst
+++ b/docs/source/tutorial/modules.rst
@@ -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
 ----------------------