ad55342 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fix syntax rule documentation

commitad553427405ffaf1f8006e6119776912cc783652 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 17 May 2015, 22:39 (11 years ago) parente8e7cd8

2 files changed+16−16

compare with master

unifiedsplit

docs/tutorial/syntax.rst+9−9 docs/tutorial/typesfuns.rst+7−7

docs/tutorial/syntax.rst+9−9

@@ -19,15 +19,15 @@ have already seen this function in Section :ref:`sect-lazy`):

1919

2020.. code-block:: idris

2121

22− boolCase : (x:Bool) -> Lazy a -> Lazy a -> a;

23− boolCase True t e = t;

24− boolCase False t e = e;

22+ ifThenElse : (x:Bool) -> Lazy a -> Lazy a -> a;

23+ ifThenElse True t e = t;

24+ ifThenElse False t e = e;

2525

2626and then extend the core syntax with a ``syntax`` declaration:

2727

2828.. code-block:: idris

2929

30− syntax "if" [test] "then" [t] "else" [e] = boolCase test t e;

30+ syntax if [test] then [t] else [e] = ifThenElse test t e;

3131

3232The left hand side of a ``syntax`` declaration describes the syntax

3333rule, and the right hand side describes its expansion. The syntax rule

@@ -58,10 +58,10 @@ recursive. The following syntax extensions would therefore be valid:

5858

5959.. code-block:: idris

6060

61− syntax [var] ":=" [val] = Assign var val;

62− syntax [test] "?" [t] ":" [e] = if test then t else e;

63− syntax "select" [x] "from" [t] "where" [w] = SelectWhere x t w;

64− syntax "select" [x] "from" [t] = Select x t;

61+ syntax [var] ":=" [val] = Assign var val;

62+ syntax [test] "?" [t] ":" [e] = if test then t else e;

63+ syntax select [x] from [t] "where" [w] = SelectWhere x t w;

64+ syntax select [x] from [t] = Select x t;

6565

6666Syntax macros can be further restricted to apply only in patterns (i.e.,

6767only on the left hand side of a pattern match clause) or only in terms

@@ -92,7 +92,7 @@ forms. For example, a ``for`` loop binds a variable on each iteration:

9292

9393.. code-block:: idris

9494

95− syntax "for" {x} "in" [xs] ":" [body] = forLoop xs (\x => body)

95+ syntax for {x} in [xs] ":" [body] = forLoop xs (\x => body)

9696

9797 main : IO ()

9898 main = do for x in [1..10]:

docs/tutorial/typesfuns.rst+7−7

@@ -586,9 +586,9 @@ not always the best approach. Consider the following function:

586586

587587.. code-block:: idris

588588

589− boolCase : Bool -> a -> a -> a;

590− boolCase True t e = t;

591− boolCase False t e = e;

589+ ifThenElse : Bool -> a -> a -> a;

590+ ifThenElse True t e = t;

591+ ifThenElse False t e = e;

592592

593593This function uses one of the ``t`` or ``e`` arguments, but not both

594594(in fact, this is used to implement the ``if...then...else`` construct

@@ -606,14 +606,14 @@ data type, which allows evaluation to be suspended:

606606A value of type ``Lazy a`` is unevaluated until it is forced by

607607``Force``. The Idris type checker knows about the ``Lazy`` type,

608608and inserts conversions where necessary between ``Lazy a`` and ``a``,

609−and vice versa. We can therefore write ``boolCase`` as follows,

609+and vice versa. We can therefore write ``ifThenElse`` as follows,

610610without any explicit use of ``Force`` or ``Delay``:

611611

612612.. code-block:: idris

613613

614− boolCase : Bool -> Lazy a -> Lazy a -> a;

615− boolCase True t e = t;

616− boolCase False t e = e;

614+ ifThenElse : Bool -> Lazy a -> Lazy a -> a;

615+ ifThenElse True t e = t;

616+ ifThenElse False t e = e;

617617

618618Useful Data Types

619619=================