@@ -105,7 +105,16 @@ Meaning for Functions
105105 definition can be used after it is imported. In other words, the
106106 definition itself is considered part of the module's interface. The
107107 long name ``public export`` is intended to make you think twice
108− about doing this...
108+ about doing this.
109+
110+.. note::
111+
112+ Type synonyms in Idris are created by writing a function. When
113+ setting the visibility for a module, it might be a good idea to
114+ ``public export`` all type synonyms if they are to be used outside
115+ the module. Otherwise, Idris won't know what the synonym is a
116+ synonym for.
117+
109118
110119Meaning for Data Types
111120----------------------
@@ -128,6 +137,7 @@ For interfaces, the meanings are:
128137 definitions are exported
129138
130139
140+
131141``BTree`` Revisited
132142+++++++++++++++++++
133143