@@ -105,7 +105,16 @@ Meaning for Functions
105 definition can be used after it is imported. In other words, the
105 definition can be used after it is imported. In other words, the
106 definition itself is considered part of the module's interface. The
106 definition itself is considered part of the module's interface. The
107 long name ``public export`` is intended to make you think twice
107 long name ``public export`` is intended to make you think twice
108− about doing this...
108+ about doing this.
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
110Meaning for Data Types
119Meaning for Data Types
111----------------------
120----------------------
@@ -128,6 +137,7 @@ For interfaces, the meanings are:
128 definitions are exported
137 definitions are exported
131``BTree`` Revisited
141``BTree`` Revisited
132+++++++++++++++++++
142+++++++++++++++++++