git.iko.soy/Idris-dev
on master help sign in
Fix syntax rule documentation
ad55342Edwin Brady
docs/tutorial/syntax.rst+9−9
compare with master
unifiedsplit
@@ -19,15 +19,15 @@ have already seen this function in Section :ref:`sect-lazy`):
19
19
20.. code-block:: idris
20.. code-block:: idris
21
21
22− boolCase : (x:Bool) -> Lazy a -> Lazy a -> a;
22+ ifThenElse : (x:Bool) -> Lazy a -> Lazy a -> a;
23− boolCase True t e = t;
23+ ifThenElse True t e = t;
24− boolCase False t e = e;
24+ ifThenElse False t e = e;
25
25
26and then extend the core syntax with a ``syntax`` declaration:
26and then extend the core syntax with a ``syntax`` declaration:
27
27
28.. code-block:: idris
28.. code-block:: idris
29
29
30− syntax "if" [test] "then" [t] "else" [e] = boolCase test t e;
30+ syntax if [test] then [t] else [e] = ifThenElse test t e;
31
31
32The left hand side of a ``syntax`` declaration describes the syntax
32The left hand side of a ``syntax`` declaration describes the syntax
33rule, and the right hand side describes its expansion. The syntax rule
33rule, and the right hand side describes its expansion. The syntax rule
@@ -58,10 +58,10 @@ recursive. The following syntax extensions would therefore be valid:
58
58
59.. code-block:: idris
59.. code-block:: idris
60
60
61− syntax [var] ":=" [val] = Assign var val;
61+ syntax [var] ":=" [val] = Assign var val;
62− syntax [test] "?" [t] ":" [e] = if test then t else e;
62+ syntax [test] "?" [t] ":" [e] = if test then t else e;
63− syntax "select" [x] "from" [t] "where" [w] = SelectWhere x t w;
63+ syntax select [x] from [t] "where" [w] = SelectWhere x t w;
64− syntax "select" [x] "from" [t] = Select x t;
64+ syntax select [x] from [t] = Select x t;
65
65
66Syntax macros can be further restricted to apply only in patterns (i.e.,
66Syntax macros can be further restricted to apply only in patterns (i.e.,
67only on the left hand side of a pattern match clause) or only in terms
67only 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:
92
92
93.. code-block:: idris
93.. code-block:: idris
94
94
95− syntax "for" {x} "in" [xs] ":" [body] = forLoop xs (\x => body)
95+ syntax for {x} in [xs] ":" [body] = forLoop xs (\x => body)
96
96
97 main : IO ()
97 main : IO ()
98 main = do for x in [1..10]:
98 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:
586
586
587.. code-block:: idris
587.. code-block:: idris
588
588
589− boolCase : Bool -> a -> a -> a;
589+ ifThenElse : Bool -> a -> a -> a;
590− boolCase True t e = t;
590+ ifThenElse True t e = t;
591− boolCase False t e = e;
591+ ifThenElse False t e = e;
592
592
593This function uses one of the ``t`` or ``e`` arguments, but not both
593This function uses one of the ``t`` or ``e`` arguments, but not both
594(in fact, this is used to implement the ``if...then...else`` construct
594(in fact, this is used to implement the ``if...then...else`` construct
@@ -606,14 +606,14 @@ data type, which allows evaluation to be suspended:
606A value of type ``Lazy a`` is unevaluated until it is forced by
606A value of type ``Lazy a`` is unevaluated until it is forced by
607``Force``. The Idris type checker knows about the ``Lazy`` type,
607``Force``. The Idris type checker knows about the ``Lazy`` type,
608and inserts conversions where necessary between ``Lazy a`` and ``a``,
608and 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,
610without any explicit use of ``Force`` or ``Delay``:
610without any explicit use of ``Force`` or ``Delay``:
611
611
612.. code-block:: idris
612.. code-block:: idris
613
613
614− boolCase : Bool -> Lazy a -> Lazy a -> a;
614+ ifThenElse : Bool -> Lazy a -> Lazy a -> a;
615− boolCase True t e = t;
615+ ifThenElse True t e = t;
616− boolCase False t e = e;
616+ ifThenElse False t e = e;
617
617
618Useful Data Types
618Useful Data Types
619=================
619=================