@@ -137,7 +137,7 @@ Unlike Haskell, there is no restriction on whether types and function
137137names must begin with a capital letter or not. Function names
138138(``plus`` and ``mult`` above), data constructors (``Z``, ``S``,
139139``Nil`` and ``::``) and type constructors (``Nat`` and ``List``) are
140−all part of the same namespace. By convention, however,
140+all part of the same namespace. By convention, however,
141141data types and constructor names typically begin with a capital letter.
142142We can test these functions at the Idris prompt:
143143
@@ -495,9 +495,19 @@ vector. For example:
495495 testVec : Vect 4 Int
496496 testVec = 3 :: 4 :: 5 :: 6 :: Nil
497497
498− inVect : IsElem 5 testVec
498+ inVect : IsElem 5 Main.testVec
499499 inVect = There (There Here)
500500
501+
502+.. important:: Implicit Arguments and Scope
503+
504+ Within the type signature the typechecker will treat all variables
505+ that start with an lowercase letter as an implicit variable. To
506+ get the above code example to compile you will need to provide a
507+ qualified name for ``testVec``. In the example above, we have
508+ assumed that the code lives within the ``Main`` module.
509+
510+
501511If the same implicit arguments are being used a lot, it can make a
502512definition difficult to read. To avoid this problem, a ``using`` block
503513gives the types and ordering of any implicit arguments which can
@@ -510,6 +520,8 @@ appear within the block:
510520 Here : IsElem x (x :: xs)
511521 There : IsElem x xs -> IsElem x (y :: xs)
512522
523+
524+
513525Note: Declaration Order and ``mutual`` blocks
514526~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
515527
@@ -583,7 +595,7 @@ example for reading and writing files, including:
583595
584596 openFile : (f : String) -> (m : Mode) -> IO (Either FileError File)
585597 closeFile : File -> IO ()
586−
598+
587599 fGetLine : (h : File) -> IO (Either FileError String)
588600 fPutStr : (h : File) -> (str : String) -> IO (Either FileError ())
589601 fEOF : File -> IO Bool