@@ -38,7 +38,7 @@ collection of declarations and definitions. In this example no imports
38have been specified. However Idris programs can consist of several
38have been specified. However Idris programs can consist of several
39modules and the definitions in each module each have their own
39modules and the definitions in each module each have their own
40namespace. This is discussed further in Section
40namespace. This is discussed further in Section
41−:ref:`sect-namespaces`). When writing Idris programs both the order in
41+:ref:`sect-namespaces`). When writing Idris programs both the order in which
42definitions are given and indentation are significant. Functions and
42definitions are given and indentation are significant. Functions and
43data types must be defined before use, incidently each definition must
43data types must be defined before use, incidently each definition must
44have a type declaration, for example see ``x : Int``, ``foo :
44have a type declaration, for example see ``x : Int``, ``foo :