75e3863 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #2244 from ulidtko/patch-1

minor docs editorials

commit75e38632fa17b9c3ff0b41234a87ab01369b91b9 authorJan de Muijnck-Hughes <jfdm@users.noreply.github.com> dateMon 11 May 2015, 14:48 (11 years ago) parentdc69794 315225f

3 files changed+29−7

compare with master

unifiedsplit

docs/proofs/patterns.rst+2−2 docs/tutorial/interp.rst+2−2 docs/tutorial/modules.rst+25−3

docs/proofs/patterns.rst+2−2

@@ -46,7 +46,7 @@ declaration. You should see:

4646 plus_commutes n m = ?plus_commutes_rhs

4747

4848To 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

5050``\c`` with the cursor over the ``n`` in the definition.) You

5151should see:

5252

@@ -334,7 +334,7 @@ defined by matching on its first argument. The complete definition is:

334334 plus_commutes_S k Z = Refl

335335 plus_commutes_S k (S j) = rewrite plus_commutes_S k j in Refl

336336

337−All metavariables have now been solved,

337+All metavariables have now been solved.

338338

339339The ``total`` annotation means that we require the final function to

340340pass 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:

213213

214214 interp env (App f s) = interp env f (interp env s)

215215

216−Operators and interpreters are, again, direct translations into the

216+Operators and conditionals are, again, direct translations into the

217217equivalent Idris constructs. For operators, we apply the function to

218218its operands directly, and for ``If``, we apply the Idris

219219``if...then...else`` construct directly.

@@ -236,7 +236,7 @@ We can make some simple test functions. Firstly, adding two inputs

236236 add = Lam (Lam (Op (+) (Var Stop) (Var (Pop Stop))))

237237

238238More 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)``),

240240can be written as:

241241

242242.. code-block:: idris

docs/tutorial/modules.rst+25−3

@@ -26,7 +26,7 @@ module which defines a binary tree type ``BTree`` (in a file

2626

2727 toList : BTree a -> List a

2828 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)

3030

3131 toTree : Ord a => List a -> BTree a

3232 toTree [] = Leaf

@@ -44,7 +44,7 @@ Then, this gives a main program (in a file

4444

4545 main : IO ()

4646 main = do let t = toTree [1,8,2,7,9,3]

47− print (btree.toList t)

47+ print (Btree.toList t)

4848

4949

5050

@@ -118,7 +118,7 @@ functions to be exported as ``abstract``, as we see below:

118118 abstract

119119 toList : BTree a -> List a

120120 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)

122122

123123 abstract

124124 toTree : Ord a => List a -> BTree a

@@ -128,6 +128,28 @@ functions to be exported as ``abstract``, as we see below:

128128Finally, the default export mode can be changed with the ``%access``

129129directive, for example:

130130

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+

131153In this case, any function with no access modifier will be exported as

132154``abstract``, rather than left ``private``.

133155