git.iko.soy/Idris-dev
on master help sign in
Merge pull request #2244 from ulidtko/patch-1
75e3863Jan de Muijnck-Hughes
docs/proofs/patterns.rst+2−2
compare with master
unifiedsplit
@@ -46,7 +46,7 @@ declaration. You should see:
46 plus_commutes n m = ?plus_commutes_rhs
46 plus_commutes n m = ?plus_commutes_rhs
47
47
48To prove this by induction on ``n``, as we sketched in Section
48To prove this by induction on ``n``, as we sketched in Section
49−[sect:induction], we begin with a case split on ``n`` (press
49+:ref:`sect-inductive`, we begin with a case split on ``n`` (press
50``\c`` with the cursor over the ``n`` in the definition.) You
50``\c`` with the cursor over the ``n`` in the definition.) You
51should see:
51should see:
52
52
@@ -334,7 +334,7 @@ defined by matching on its first argument. The complete definition is:
334 plus_commutes_S k Z = Refl
334 plus_commutes_S k Z = Refl
335 plus_commutes_S k (S j) = rewrite plus_commutes_S k j in Refl
335 plus_commutes_S k (S j) = rewrite plus_commutes_S k j in Refl
336
336
337−All metavariables have now been solved,
337+All metavariables have now been solved.
338
338
339The ``total`` annotation means that we require the final function to
339The ``total`` annotation means that we require the final function to
340pass the totality checker; i.e. it will terminate on all possible
340pass the totality checker; i.e. it will terminate on all possible
docs/tutorial/interp.rst+2−2
@@ -213,7 +213,7 @@ because of its type:
213
213
214 interp env (App f s) = interp env f (interp env s)
214 interp env (App f s) = interp env f (interp env s)
215
215
216−Operators and interpreters are, again, direct translations into the
216+Operators and conditionals are, again, direct translations into the
217equivalent Idris constructs. For operators, we apply the function to
217equivalent Idris constructs. For operators, we apply the function to
218its operands directly, and for ``If``, we apply the Idris
218its operands directly, and for ``If``, we apply the Idris
219``if...then...else`` construct directly.
219``if...then...else`` construct directly.
@@ -236,7 +236,7 @@ We can make some simple test functions. Firstly, adding two inputs
236 add = Lam (Lam (Op (+) (Var Stop) (Var (Pop Stop))))
236 add = Lam (Lam (Op (+) (Var Stop) (Var (Pop Stop))))
237
237
238More interestingly, a factorial function ``fact``
238More interestingly, a factorial function ``fact``
239−(e.g. ``\. if (x == 0) then 1 else (fact (x-1) * x)``),
239+(e.g. ``\x. if (x == 0) then 1 else (fact (x-1) * x)``),
240can be written as:
240can be written as:
241
241
242.. code-block:: idris
242.. code-block:: idris
docs/tutorial/modules.rst+25−3
@@ -26,7 +26,7 @@ module which defines a binary tree type ``BTree`` (in a file
26
26
27 toList : BTree a -> List a
27 toList : BTree a -> List a
28 toList Leaf = []
28 toList Leaf = []
29− toList (Node l v r) = btree.toList l ++ (v :: btree.toList r)
29+ toList (Node l v r) = Btree.toList l ++ (v :: Btree.toList r)
30
30
31 toTree : Ord a => List a -> BTree a
31 toTree : Ord a => List a -> BTree a
32 toTree [] = Leaf
32 toTree [] = Leaf
@@ -44,7 +44,7 @@ Then, this gives a main program (in a file
44
44
45 main : IO ()
45 main : IO ()
46 main = do let t = toTree [1,8,2,7,9,3]
46 main = do let t = toTree [1,8,2,7,9,3]
47− print (btree.toList t)
47+ print (Btree.toList t)
48
48
49
49
50
50
@@ -118,7 +118,7 @@ functions to be exported as ``abstract``, as we see below:
118 abstract
118 abstract
119 toList : BTree a -> List a
119 toList : BTree a -> List a
120 toList Leaf = []
120 toList Leaf = []
121− toList (Node l v r) = btree.toList l ++ (v :: btree.toList r)
121+ toList (Node l v r) = Btree.toList l ++ (v :: Btree.toList r)
122
122
123 abstract
123 abstract
124 toTree : Ord a => List a -> BTree a
124 toTree : Ord a => List a -> BTree a
@@ -128,6 +128,28 @@ functions to be exported as ``abstract``, as we see below:
128Finally, the default export mode can be changed with the ``%access``
128Finally, the default export mode can be changed with the ``%access``
129directive, for example:
129directive, for example:
130
130
131+.. code-block:: idris
132+
133+ module Btree
134+
135+ %access abstract
136+
137+ data BTree a = Leaf
138+ | Node (BTree a) a (BTree a)
139+
140+ insert : Ord a => a -> BTree a -> BTree a
141+ insert x Leaf = Node Leaf x Leaf
142+ insert x (Node l v r) = if (x < v) then (Node (insert x l) v r)
143+ else (Node l v (insert x r))
144+
145+ toList : BTree a -> List a
146+ toList Leaf = []
147+ toList (Node l v r) = Btree.toList l ++ (v :: Btree.toList r)
148+
149+ toTree : Ord a => List a -> BTree a
150+ toTree [] = Leaf
151+ toTree (x :: xs) = insert x (toTree xs)
152+
131In this case, any function with no access modifier will be exported as
153In this case, any function with no access modifier will be exported as
132``abstract``, rather than left ``private``.
154``abstract``, rather than left ``private``.
133
155