@@ -56,7 +56,7 @@ answer. For example:
58 *prims> 6*6+6
58 *prims> 6*6+6
59− 42 : Int
59+ 42 : Integer
60 *prims> x == 6*6+6
60 *prims> x == 6*6+6
61 True : Bool
61 True : Bool
@@ -792,12 +792,12 @@ providing a default value:
793.. code-block:: idris
793.. code-block:: idris
795− maybe : Lazy b -> (a -> b) -> Maybe a -> b
795+ maybe : Lazy b -> Lazy (a -> b) -> Maybe a -> b
797−Note that the type of the first argument is ``Lazy b`` rather than
797+Note that the types of the first two arguments are wrapped in
798−simply ``b``. Since the default value might not be used, we mark it as
798+``Lazy``. Since only one of the two arguments will actually be used,
799−``Lazy`` in case it is a large expression where evaluating it then
799+we mark them as ``Lazy`` in case they are large expressions where it
800−discarding it would be wasteful.
800+would be wasteful to compute and then discard them.
@@ -820,6 +820,15 @@ contain an arbitrary number of values, represented as nested pairs:
820 jim : (String, Int, String)
820 jim : (String, Int, String)
821 jim = ("Jim", 25, "Cambridge")
821 jim = ("Jim", 25, "Cambridge")
825+ *usefultypes> fst jim
827+ *usefultypes> snd jim
828+ (25, "Cambridge") : (Int, String)
829+ *usefultypes> jim == ("Jim", (25, "Cambridge"))
823Dependent Pairs
832Dependent Pairs
824---------------
833---------------
@@ -1025,7 +1034,11 @@ For example:
1025 className : String
1034 className : String
1027**Note** that it is no longer possible to use the ``addStudent``
1036**Note** that it is no longer possible to use the ``addStudent``
1028−method from earlier as that would change the size of the class. To provide an add student the function must specify in the type that the size of the class has been increased by one. As the size if specified using natural numbers, the new value can be incremented using the successor constructor.
1037+method from earlier as that would change the size of the class. A
1038+method to add a student must now specify in the type that the
1039+size of the class has been increased by one. As the size is specified
1040+using natural numbers, the new value can be incremented using the
1030.. code-block:: idris
1043.. code-block:: idris
@@ -1137,8 +1150,8 @@ auxiliary functions, and is also used internally to implement pattern
1137matching ``let`` and lambda bindings. It will *only* work if:
1150matching ``let`` and lambda bindings. It will *only* work if:
1139- Each branch *matches* a value of the same type, and *returns* a
1152- Each branch *matches* a value of the same type, and *returns* a
1140− value of the same type.
1153+ value of the same type.
1142- The type of the result is "known". i.e. the type of the expression
1155- The type of the result is "known". i.e. the type of the expression
1143− can be determined *without* type checking the ``case``-expression
1156+ can be determined *without* type checking the ``case``-expression
1144− itself.
1157+ itself.