git.iko.soy/Idris-dev
on master help sign in
Update where type inference example in tutorial
d79a445Edwin Brady
tutorial/examples/wheres.idrnew file+14
compare with master
unifiedsplit
@@ -0,0 +1,14 @@
1+module wheres
2+
3+even : Nat -> Bool
4+even O = True
5+even (S k) = odd k where
6+ odd O = False
7+ odd (S k) = even k
8+
9+test : List Nat
10+test = [c (S 1), c O, d (S O)]
11+ where c x = 42 + x
12+ d y = c (y + 1 + z y)
13+ where z w = y + w
14+
tutorial/typesfuns.tex+5−5
@@ -257,11 +257,11 @@ even (S k) = odd k where
257 odd O = False
257 odd O = False
258 odd (S k) = even k
258 odd (S k) = even k
259
259
260−test : Num a => List a
260+test : List Nat
261−test = [c 1, c 2, d 3]
261+test = [c (S 1), c O, d (S O)]
262− where c x = 42 + x
262+ where c x = 42 + x
263− d y = c (y + 1 + z y)
263+ d y = c (y + 1 + z y)
264− where z w = y + w
264+ where z w = y + w
265
265
266\end{SaveVerbatim}
266\end{SaveVerbatim}
267\useverb{whereinfer}
267\useverb{whereinfer}