32fc703 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #3034 from jfdm/doc-fixes

32fc703Jan de Muijnck-Hughes11 years ago

docs/effects/simpleeff.rst+11−10

compare with master

unifiedsplit

@@ -578,16 +578,17 @@ this simply by updating the type of ``eval`` to include ``STDIO``.

578

579 eval : Expr -> Eff Integer [STDIO, EXCEPTION String, RND, STATE Env]

580

581−Note that using ``STDIO`` will restrict the number of contexts in

581+.. note:: Using ``STDIO`` will restrict the number of contexts in

582−which ``eval`` can be ``run`` to those which support ``STDIO``, such

582+ which ``eval`` can be ``run`` to those which support

583−as ``IO``. Once effect lists get longer, it can be a good idea instead

583+ ``STDIO``, such as ``IO``. Once effect lists get longer, it

584+ can be a good idea instead to encapsulate sets of effects in

584−to encapsulate sets of effects in a type synonym. This is achieved as

585+ a type synonym. This is achieved as follows, simply by

585−follows, simply by defining a function which computes a type, since

586+ defining a function which computes a type, since types are

586−types are first class in Idris:

587+ first class in Idris:

587

588

588−.. code-block:: idris

589+ .. code-block:: idris

589

590

590− EvalEff : Type -> Type

591+ EvalEff : Type -> Type

591− EvalEff t = Eff t [STDIO, EXCEPTION String, RND, STATE Env]

592+ EvalEff t = Eff t [STDIO, EXCEPTION String, RND, STATE Env]

592

593

593− eval : Expr -> EvalEff Integer

594+ eval : Expr -> EvalEff Integer

docs/tutorial/typesfuns.rst+16−3

@@ -137,7 +137,7 @@ Unlike Haskell, there is no restriction on whether types and function

137names must begin with a capital letter or not. Function names

138(``plus`` and ``mult`` above), data constructors (``Z``, ``S``,

139``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,

141data types and constructor names typically begin with a capital letter.

142We can test these functions at the Idris prompt:

143

@@ -495,9 +495,20 @@ vector. For example:

495 testVec : Vect 4 Int

496 testVec = 3 :: 4 :: 5 :: 6 :: Nil

497

498− inVect : IsElem 5 testVec

498+ inVect : IsElem 5 Main.testVec

499 inVect = There (There Here)

500

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 **and** are not applied to

506+ something else as an implicit variable. To get the above code

507+ example to compile you will need to provide a qualified name for

508+ ``testVec``. In the example above, we have assumed that the code

509+ lives within the ``Main`` module.

510+

511+

501If the same implicit arguments are being used a lot, it can make a

512If the same implicit arguments are being used a lot, it can make a

502definition difficult to read. To avoid this problem, a ``using`` block

513definition difficult to read. To avoid this problem, a ``using`` block

503gives the types and ordering of any implicit arguments which can

514gives the types and ordering of any implicit arguments which can

@@ -510,6 +521,8 @@ appear within the block:

510 Here : IsElem x (x :: xs)

521 Here : IsElem x (x :: xs)

511 There : IsElem x xs -> IsElem x (y :: xs)

522 There : IsElem x xs -> IsElem x (y :: xs)

512

523

524+

525+

513Note: Declaration Order and ``mutual`` blocks

526Note: Declaration Order and ``mutual`` blocks

514~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

527~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

515

528

@@ -583,7 +596,7 @@ example for reading and writing files, including:

583

596

584 openFile : (f : String) -> (m : Mode) -> IO (Either FileError File)

597 openFile : (f : String) -> (m : Mode) -> IO (Either FileError File)

585 closeFile : File -> IO ()

598 closeFile : File -> IO ()

586−

599+

587 fGetLine : (h : File) -> IO (Either FileError String)

600 fGetLine : (h : File) -> IO (Either FileError String)

588 fPutStr : (h : File) -> (str : String) -> IO (Either FileError ())

601 fPutStr : (h : File) -> (str : String) -> IO (Either FileError ())

589 fEOF : File -> IO Bool

602 fEOF : File -> IO Bool