@@ -38,7 +38,7 @@ collection of declarations and definitions. In this example no imports
3838have been specified. However Idris programs can consist of several
3939modules and the definitions in each module each have their own
4040namespace. 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
4242definitions are given and indentation are significant. Functions and
4343data types must be defined before use, incidently each definition must
4444have a type declaration, for example see ``x : Int``, ``foo :