2e9fcd4 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Remove semicolons in tutorial

2e9fcd4Edwin Brady15 years ago

lib/io.idr+22−22

compare with master

unifiedsplit

@@ -1,46 +1,46 @@

1−import prelude.list;

1+import prelude.list

3%access public

5−abstract data IO a = prim__IO a;

5+abstract data IO a = prim__IO a

7abstract

8−io_bind : IO a -> (a -> IO b) -> IO b;

8+io_bind : IO a -> (a -> IO b) -> IO b

9−io_bind (prim__IO v) k = k v;

9+io_bind (prim__IO v) k = k v

11abstract

12−io_return : a -> IO a;

12+io_return : a -> IO a

13−io_return x = prim__IO x;

13+io_return x = prim__IO x

15-- This may seem pointless, but we can use it to force an

16-- evaluation of main that Epic wouldn't otherwise do...

18−-- run__IO : IO () -> IO ();

18+-- run__IO : IO () -> IO ()

19−-- run__IO (prim__IO v) = prim__IO v;

19+-- run__IO (prim__IO v) = prim__IO v

23−interpFTy : FTy -> Set;

23+interpFTy : FTy -> Set

24−interpFTy FInt = Int;

24+interpFTy FInt = Int

25−interpFTy FFloat = Float;

25+interpFTy FFloat = Float

26−interpFTy FChar = Char;

26+interpFTy FChar = Char

27−interpFTy FString = String;

27+interpFTy FString = String

28−interpFTy FPtr = Ptr;

28+interpFTy FPtr = Ptr

29−interpFTy FUnit = ();

29+interpFTy FUnit = ()

31−ForeignTy : (xs:List FTy) -> (t:FTy) -> Set;

31+ForeignTy : (xs:List FTy) -> (t:FTy) -> Set

32ForeignTy xs t = mkForeign' (rev xs) (IO (interpFTy t)) where {

33− mkForeign' : List FTy -> Set -> Set;

33+ mkForeign' : List FTy -> Set -> Set

34− mkForeign' Nil ty = ty;

34+ mkForeign' Nil ty = ty

35− mkForeign' (s :: ss) ty = mkForeign' ss (interpFTy s -> ty);

35+ mkForeign' (s :: ss) ty = mkForeign' ss (interpFTy s -> ty)

36}

39data Foreign : Set -> Set where

40 FFun : String -> (xs:List FTy) -> (t:FTy) ->

41− Foreign (ForeignTy xs t);

41+ Foreign (ForeignTy xs t)

43−mkForeign : Foreign x -> x;

43+mkForeign : Foreign x -> x

44-- mkForeign compiled as primitive

src/Idris/Prover.hs+1−1

@@ -28,7 +28,7 @@ prover x = do ctxt <- getContext

28showProof :: Name -> [String] -> String

29showProof n ps = show n ++ " = proof {" ++ "\n" ++

30 showSep "\n" (map (\x -> " " ++ x ++ ";") ps) ++

31− "\n};\n"

31+ "\n}\n"

33prove :: Context -> Name -> Type -> Idris ()

34prove ctxt n ty

tutorial/classes.tex+46−46

@@ -17,7 +17,7 @@ provides an interface for converting values to

17\begin{SaveVerbatim}{showclass}

19class Show a where {

20− show : a -> String;

20+ show : a -> String

21}

23\end{SaveVerbatim}

@@ -29,7 +29,7 @@ This generates a function of the following type (which we call a \emph{method} o

30\begin{SaveVerbatim}{showty}

32−show : Show a => a -> String;

32+show : Show a => a -> String

34\end{SaveVerbatim}

35\useverb{showty}

@@ -44,8 +44,8 @@ could be defined as:

44\begin{SaveVerbatim}{shownat}

46instance Show Nat where {

47− show O = "O";

47+ show O = "O"

48− show (S k) = "s" ++ show k;

48+ show (S k) = "s" ++ show k

49}

51Idris> show (S (S (S O)))

@@ -64,10 +64,10 @@ to a \texttt{String}:

65instance Show a => Show (Vect a n) where {

66 show xs = "[" ++ show' xs ++ "]" where {

67− show' : Show a => Vect a n -> String;

67+ show' : Show a => Vect a n -> String

68− show' VNil = "";

68+ show' VNil = ""

69− show' (x :: VNil) = show x;

69+ show' (x :: VNil) = show x

70− show' (x :: xs) = show x ++ ", " ++ show' xs;

70+ show' (x :: xs) = show x ++ ", " ++ show' xs

71 }

72}

@@ -82,8 +82,8 @@ values for equality or inequality, with instances for all of the built-in types:

82\begin{SaveVerbatim}{eqbasic}

84class Eq a where {

85− (==) : a -> a -> Bool;

85+ (==) : a -> a -> Bool

86− (/=) : a -> a -> Bool;

86+ (/=) : a -> a -> Bool

87}

89\end{SaveVerbatim}

@@ -96,12 +96,12 @@ For example, for an instance of \texttt{Eq} for \texttt{Nat}:

96\begin{SaveVerbatim}{eqnat}

98instance Eq Nat where {

99− O == O = True;

99+ O == O = True

100− (S x) == (S y) = x == y;

100+ (S x) == (S y) = x == y

101− O == (S y) = False;

101+ O == (S y) = False

102− (S x) == O = False;

102+ (S x) == O = False

103

104− x /= y = not (x == y);

104+ x /= y = not (x == y)

105}

106

107\end{SaveVerbatim}

@@ -116,11 +116,11 @@ declaration, in terms of the other method:

116\begin{SaveVerbatim}{eqdefault}

117

118class Eq a where {

119− (==) : a -> a -> Bool;

119+ (==) : a -> a -> Bool

120− (/=) : a -> a -> Bool;

120+ (/=) : a -> a -> Bool

121

122− x /= y = not (x == y);

122+ x /= y = not (x == y)

123− y == y = not (x /= y);

123+ y == y = not (x /= y)

124}

125

126\end{SaveVerbatim}

@@ -139,7 +139,7 @@ which inherits method from \texttt{Eq} as well as defining some of its own:

139

140\begin{SaveVerbatim}{ord}

141

142−data Ordering = LT | EQ | GT;

142+data Ordering = LT | EQ | GT

143

144\end{SaveVerbatim}

145\useverb{ord}

@@ -147,14 +147,14 @@ data Ordering = LT | EQ | GT;

147\begin{SaveVerbatim}{eqord}

148

149class Eq a => Ord a where {

150− compare : a -> a -> Ordering;

150+ compare : a -> a -> Ordering

151−

151+

152− (<) : a -> a -> Bool;

152+ (<) : a -> a -> Bool

153− (>) : a -> a -> Bool;

153+ (>) : a -> a -> Bool

154− (<=) : a -> a -> Bool;

154+ (<=) : a -> a -> Bool

155− (>=) : a -> a -> Bool;

155+ (>=) : a -> a -> Bool

156− max : a -> a -> a;

156+ max : a -> a -> a

157− min : a -> a -> a;

157+ min : a -> a -> a

158}

159

160\end{SaveVerbatim}

@@ -171,7 +171,7 @@ function type to the right of the fat arrow:

171

172\begin{SaveVerbatim}{sortty}

173

174−sort : Ord a => List a -> List a;

174+sort : Ord a => List a -> List a

175

176\end{SaveVerbatim}

177\useverb{sortty}

@@ -182,8 +182,8 @@ written in brackets in a comma separated list, for example:

182

183\begin{SaveVerbatim}{sortshow}

184

185−sortAndShow : (Ord a, Show a) => List a -> String;

185+sortAndShow : (Ord a, Show a) => List a -> String

186−sortAndShow xs = show (sort xs);

186+sortAndShow xs = show (sort xs)

187

188\end{SaveVerbatim}

189\useverb{sortshow}

@@ -201,8 +201,8 @@ declaration. For example:

201\begin{SaveVerbatim}{monad}

202

203class Monad (m : Set -> Set) where {

204− return : a -> m a;

204+ return : a -> m a

205− (>>=) : m a -> (a -> m b) -> m b;

205+ (>>=) : m a -> (a -> m b) -> m b

206}

207

208\end{SaveVerbatim}

@@ -226,10 +226,10 @@ We can also define an instance for \texttt{Maybe}, as follows:

226\begin{SaveVerbatim}{maybemonad}

227

228instance Monad Maybe where {

229− return = Just;

229+ return = Just

230

231− Nothing >>= k = Nothing;

231+ Nothing >>= k = Nothing

232− (Just x) >>= k = k x;

232+ (Just x) >>= k = k x

233}

234

235\end{SaveVerbatim}

@@ -241,11 +241,11 @@ Using this we can, for example, define a function which adds two

241

242\begin{SaveVerbatim}{maybeadd}

243

244−m_add : Maybe Int -> Maybe Int -> Maybe Int;

244+m_add : Maybe Int -> Maybe Int -> Maybe Int

245−m_add x y = do { x' <- x; -- Extract value from x

245+m_add x y = do { x' <- x -- Extract value from x

246− y' <- y; -- Extract value from y

246+ y' <- y -- Extract value from y

247− return (x' + y'); -- Add them

247+ return (x' + y') -- Add them

248− };

248+ }

249

250\end{SaveVerbatim}

251\useverb{maybeadd}

@@ -274,8 +274,8 @@ general, and applies to anything which is an instance of \texttt{MonadPlus}:

274\begin{SaveVerbatim}{monadplus}

275

276class Monad m => MonadPlus (m : Set -> Set) where {

277− mplus : m a -> m a -> m a;

277+ mplus : m a -> m a -> m a

278− mzero : m a;

278+ mzero : m a

279}

280

281\end{SaveVerbatim}

@@ -299,7 +299,7 @@ the following function:

299

300\begin{SaveVerbatim}{guardq}

301

302−guard : MonadPlus m => Bool -> m ();

302+guard : MonadPlus m => Bool -> m ()

303

304\end{SaveVerbatim}

305\useverb{guardq}

@@ -319,8 +319,8 @@ Using monad comprehensions, an alternative definition for \texttt{m\_add} would

319

320\begin{SaveVerbatim}{maddb}

321

322−m_add : Maybe Int -> Maybe Int -> Maybe Int;

322+m_add : Maybe Int -> Maybe Int -> Maybe Int

323−m_add x y = [ x' + y' | x' <- x, y' <- y ];

323+m_add x y = [ x' + y' | x' <- x, y' <- y ]

324\end{SaveVerbatim}

325\useverb{maddb}

326

tutorial/examples/Makefilenew file+7

@@ -0,0 +1,7 @@

1+check: .PHONY

2+ for x in *.idr ; do \

3+ echo "Checking $$x"; \

4+ idris --check $$x; \

5+ done

7+.PHONY:

tutorial/examples/binary.idr+27−27

@@ -1,45 +1,45 @@

1−module main;

1+module main

3data Binary : Nat -> Set where

4 bEnd : Binary O

5 | bO : Binary n -> Binary (n + n)

6− | bI : Binary n -> Binary (S (n + n));

6+ | bI : Binary n -> Binary (S (n + n))

8instance Show (Binary n) where {

9− show (bO x) = show x ++ "0";

9+ show (bO x) = show x ++ "0"

10− show (bI x) = show x ++ "1";

10+ show (bI x) = show x ++ "1"

11− show bEnd = "";

11+ show bEnd = ""

12}

14data Parity : Nat -> Set where

15 even : Parity (n + n)

16− | odd : Parity (S (n + n));

16+ | odd : Parity (S (n + n))

18−parity : (n:Nat) -> Parity n;

18+parity : (n:Nat) -> Parity n

19−parity O = even {n=O};

19+parity O = even {n=O}

20−parity (S O) = odd {n=O};

20+parity (S O) = odd {n=O}

21parity (S (S k)) with parity k {

22− parity (S (S (j + j))) | even ?= even {n=S j};

22+ parity (S (S (j + j))) | even ?= even {n=S j}

23− parity (S (S (S (j + j)))) | odd ?= odd {n=S j};

23+ parity (S (S (S (j + j)))) | odd ?= odd {n=S j}

24}

26−natToBin : (n:Nat) -> Binary n;

26+natToBin : (n:Nat) -> Binary n

27−natToBin O = bEnd;

27+natToBin O = bEnd

28natToBin (S k) with parity k {

29− natToBin (S (j + j)) | even = bI (natToBin j);

29+ natToBin (S (j + j)) | even = bI (natToBin j)

30− natToBin (S (S (j + j))) | odd ?= bO (natToBin (S j));

30+ natToBin (S (S (j + j))) | odd ?= bO (natToBin (S j))

31}

33−intToNat : Int -> Nat;

33+intToNat : Int -> Nat

34−intToNat 0 = O;

34+intToNat 0 = O

35−intToNat x = if (x>0) then (S (intToNat (x-1))) else O;

35+intToNat x = if (x>0) then (S (intToNat (x-1))) else O

37−main : IO ();

37+main : IO ()

38−main = do { putStr "Enter a number: ";

38+main = do { putStr "Enter a number: "

39− x <- getLine;

39+ x <- getLine

40− let n = prim__strToInt x;

40+ let n = prim__strToInt x

41− let b = natToBin (fromInteger n);

41+ let b = natToBin (fromInteger n)

42− print b; };

42+ print b }

44---------- Proofs ----------

@@ -48,20 +48,20 @@ natToBin_lemma_1 = proof {

48 intro;

49 rewrite plusn_Sm j j;

50 trivial;

51−};

51+}

53parity_lemma_2 = proof {

54 intro;

55 intro;

56 rewrite plusn_Sm j j;

57 trivial;

58−};

58+}

60parity_lemma_1 = proof {

61 intro j;

62 intro;

63 rewrite plusn_Sm j j;

64 trivial;

65−};

65+}

tutorial/examples/bmain.idr+6−6

@@ -1,9 +1,9 @@

1−module main;

1+module main

3−import btree;

3+import btree

5−main : IO ();

5+main : IO ()

6−main = do { let t = toTree [1,8,2,7,9,3];

6+main = do { let t = toTree [1,8,2,7,9,3]

7− print (toList t);

7+ print (toList t)

8− };

8+ }

tutorial/examples/btree.idr+11−11

@@ -1,18 +1,18 @@

1−module btree;

1+module btree

3data BTree a = Leaf

4− | Node (BTree a) a (BTree a);

4+ | Node (BTree a) a (BTree a)

6−insert : Ord a => a -> BTree a -> BTree a;

6+insert : Ord a => a -> BTree a -> BTree a

7−insert x Leaf = Node Leaf x Leaf;

7+insert x Leaf = Node Leaf x Leaf

8insert x (Node l v r) = if (x < v) then (Node (insert x l) v r)

9− else (Node l v (insert x r));

9+ else (Node l v (insert x r))

11−toList : BTree a -> List a;

11+toList : BTree a -> List a

12−toList Leaf = [];

12+toList Leaf = []

13−toList (Node l v r) = app (toList l) (v :: toList r);

13+toList (Node l v r) = app (toList l) (v :: toList r)

15−toTree : Ord a => List a -> BTree a;

15+toTree : Ord a => List a -> BTree a

16−toTree [] = Leaf;

16+toTree [] = Leaf

17−toTree (x :: xs) = insert x (toTree xs);

17+toTree (x :: xs) = insert x (toTree xs)

tutorial/examples/classes.idr+9−9

@@ -1,11 +1,11 @@

1−m_add : Maybe Int -> Maybe Int -> Maybe Int;

1+m_add : Maybe Int -> Maybe Int -> Maybe Int

2−m_add x y = do { x' <- x; -- Extract value from x

2+m_add x y = do { x' <- x -- Extract value from x

3− y' <- y; -- Extract value from y

3+ y' <- y -- Extract value from y

4− return (x' + y'); -- Add them

4+ return (x' + y') -- Add them

5− };

5+ }

7−m_add' : Maybe Int -> Maybe Int -> Maybe Int;

7+m_add' : Maybe Int -> Maybe Int -> Maybe Int

8−m_add' x y = [ x' + y' | x' <- x, y' <- y ];

8+m_add' x y = [ x' + y' | x' <- x, y' <- y ]

10−sortAndShow : (Ord a, Show a) => List a -> String;

10+sortAndShow : (Ord a, Show a) => List a -> String

11−sortAndShow xs = show (sort xs);

11+sortAndShow xs = show (sort xs)

tutorial/examples/foo.idr+5−5

@@ -1,12 +1,12 @@

1−module foo;

1+module foo

3namespace x {

4− test : Int -> Int;

4+ test : Int -> Int

5− test x = x * 2;

5+ test x = x * 2

8namespace y {

9− test : String -> String;

9+ test : String -> String

10− test x = x ++ x;

10+ test x = x ++ x

11}

tutorial/examples/hello.idr+3−3

@@ -1,5 +1,5 @@

1−module main;

1+module main

3−main : IO ();

3+main : IO ()

4−main = putStrLn "Hello world";

4+main = putStrLn "Hello world"

tutorial/examples/interp.idr+36−36

@@ -1,25 +1,25 @@

1−module main;

1+module main

3−data Ty = TyInt | TyBool| TyFun Ty Ty;

3+data Ty = TyInt | TyBool| TyFun Ty Ty

5−interpTy : Ty -> Set;

5+interpTy : Ty -> Set

6−interpTy TyInt = Int;

6+interpTy TyInt = Int

7−interpTy TyBool = Bool;

7+interpTy TyBool = Bool

8−interpTy (TyFun s t) = interpTy s -> interpTy t;

8+interpTy (TyFun s t) = interpTy s -> interpTy t

10using (G : Vect Ty n) {

12 data Env : Vect Ty n -> Set where

13 Nil : Env Nil

14− | (::) : interpTy a -> Env G -> Env (a :: G);

14+ | (::) : interpTy a -> Env G -> Env (a :: G)

16 data HasType : (i : Fin n) -> Vect Ty n -> Ty -> Set where

17 stop : HasType fO (t :: G) t

18− | pop : HasType k G t -> HasType (fS k) (u :: G) t;

18+ | pop : HasType k G t -> HasType (fS k) (u :: G) t

20− lookup : HasType i G t -> Env G -> interpTy t;

20+ lookup : HasType i G t -> Env G -> interpTy t

21− lookup stop (x :: xs) = x;

21+ lookup stop (x :: xs) = x

22− lookup (pop k) (x :: xs) = lookup k xs;

22+ lookup (pop k) (x :: xs) = lookup k xs

24 data Expr : Vect Ty n -> Ty -> Set where

25 Var : HasType i G t -> Expr G t

@@ -28,41 +28,41 @@ using (G : Vect Ty n) {

28 | App : Expr G (TyFun a t) -> Expr G a -> Expr G t

29 | Op : (interpTy a -> interpTy b -> interpTy c) -> Expr G a -> Expr G b ->

30 Expr G c

31− | If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a;

31+ | If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a

33− interp : Env G -> {static} Expr G t -> interpTy t;

33+ interp : Env G -> {static} Expr G t -> interpTy t

34− interp env (Var i) = lookup i env;

34+ interp env (Var i) = lookup i env

35− interp env (Val x) = x;

35+ interp env (Val x) = x

36− interp env (Lam sc) = \x => interp (x :: env) sc;

36+ interp env (Lam sc) = \x => interp (x :: env) sc

37− interp env (App f s) = (interp env f) (interp env s);

37+ interp env (App f s) = (interp env f) (interp env s)

38− interp env (Op op x y) = op (interp env x) (interp env y);

38+ interp env (Op op x y) = op (interp env x) (interp env y)

39− interp env (If x t e) = if (interp env x) then (interp env t) else (interp env e);

39+ interp env (If x t e) = if (interp env x) then (interp env t) else (interp env e)

41− eId : Expr G (TyFun TyInt TyInt);

41+ eId : Expr G (TyFun TyInt TyInt)

42− eId = Lam (Var stop);

42+ eId = Lam (Var stop)

44− eAdd : Expr G (TyFun TyInt (TyFun TyInt TyInt));

44+ eAdd : Expr G (TyFun TyInt (TyFun TyInt TyInt))

45− eAdd = Lam (Lam (Op (+) (Var stop) (Var (pop stop))));

45+ eAdd = Lam (Lam (Op (+) (Var stop) (Var (pop stop))))

47− eDouble : Expr G (TyFun TyInt TyInt);

47+ eDouble : Expr G (TyFun TyInt TyInt)

48− eDouble = Lam (App (App eAdd (Var stop)) (Var stop));

48+ eDouble = Lam (App (App eAdd (Var stop)) (Var stop))

50− app : |(f : Expr G (TyFun a t)) -> Expr G a -> Expr G t;

50+ app : |(f : Expr G (TyFun a t)) -> Expr G a -> Expr G t

51− app = \f, a => App f a;

51+ app = \f, a => App f a

53− fact : Expr G (TyFun TyInt TyInt);

53+ fact : Expr G (TyFun TyInt TyInt)

54 fact = Lam (If (Op (==) (Var stop) (Val 0))

55− (Val 1) (Op (*) (app fact (Op (-) (Var stop) (Val 1))) (Var stop)));

55+ (Val 1) (Op (*) (app fact (Op (-) (Var stop) (Val 1))) (Var stop)))

57}

59−testFac : Int;

59+testFac : Int

60−testFac = interp [] fact 4;

60+testFac = interp [] fact 4

62−main : IO ();

62+main : IO ()

63−main = do { putStr "Enter a number: ";

63+main = do { putStr "Enter a number: "

64− x <- getLine;

64+ x <- getLine

65− print (interp [] fact (prim__strToInt x));

65+ print (interp [] fact (prim__strToInt x))

66− };

66+ }

tutorial/examples/letbind.idr+8−8

@@ -1,17 +1,17 @@

1−module letbind;

1+module letbind

3−mirror : List a -> List a;

3+mirror : List a -> List a

4mirror xs = let xs' = rev xs in

5− app xs xs';

5+ app xs xs'

7−data Person = MkPerson String Int;

7+data Person = MkPerson String Int

9−showPerson : Person -> String;

9+showPerson : Person -> String

10showPerson p = let MkPerson name age = p in

11− name ++ " is " ++ show age ++ " years old";

11+ name ++ " is " ++ show age ++ " years old"

13−splitAt : Char -> String -> (String, String);

13+splitAt : Char -> String -> (String, String)

14splitAt c x = case break (== c) x of {

15 (x, y) => (x, strTail y)

16− };

16+ }

tutorial/examples/prims.idr+9−9

@@ -1,14 +1,14 @@

1−module prims;

1+module prims

3−x : Int;

3+x : Int

4−x = 42;

4+x = 42

6−foo : String;

6+foo : String

7−foo = "Sausage machine";

7+foo = "Sausage machine"

9−bar : Char;

9+bar : Char

10−bar = 'Z';

10+bar = 'Z'

12−quux : Bool;

12+quux : Bool

13−quux = False;

13+quux = False

tutorial/examples/theorems.idr+17−17

@@ -1,25 +1,25 @@

2−fiveIsFive : 5 = 5;

2+fiveIsFive : 5 = 5

3−fiveIsFive = refl;

3+fiveIsFive = refl

5−twoPlusTwo : 2 + 2 = 4;

5+twoPlusTwo : 2 + 2 = 4

6−twoPlusTwo = refl;

6+twoPlusTwo = refl

8−plusReduces : (n:Nat) -> plus O n = n;

8+plusReduces : (n:Nat) -> plus O n = n

9−plusReduces n = refl;

9+plusReduces n = refl

11−plusReducesO : (n:Nat) -> n = plus n O;

11+plusReducesO : (n:Nat) -> n = plus n O

12−plusReducesO O = refl;

12+plusReducesO O = refl

13−plusReducesO (S k) = eqRespS (plusReducesO k);

13+plusReducesO (S k) = eqRespS (plusReducesO k)

15−plusReducesS : (n:Nat) -> (m:Nat) -> S (plus n m) = plus n (S m);

15+plusReducesS : (n:Nat) -> (m:Nat) -> S (plus n m) = plus n (S m)

16−plusReducesS O m = refl;

16+plusReducesS O m = refl

17−plusReducesS (S k) m = eqRespS (plusReducesS k m);

17+plusReducesS (S k) m = eqRespS (plusReducesS k m)

19−plusReducesO' : (n:Nat) -> n = plus n O;

19+plusReducesO' : (n:Nat) -> n = plus n O

20−plusReducesO' O = ?plusredO_O;

20+plusReducesO' O = ?plusredO_O

21plusReducesO' (S k) = let ih = plusReducesO' k in

22− ?plusredO_S;

22+ ?plusredO_S

25---------- Proofs ----------

@@ -29,10 +29,10 @@ plusredO_S = proof {

29 intro;

30 rewrite ih;

31 trivial;

32−};

32+}

34plusredO_O = proof {

35 compute;

36 trivial;

37−};

37+}

tutorial/examples/usefultypes.idr+12−12

@@ -1,21 +1,21 @@

2−intVec : Vect Int 5;

2+intVec : Vect Int 5

3−intVec = [1, 2, 3, 4, 5];

3+intVec = [1, 2, 3, 4, 5]

5−double : Int -> Int;

5+double : Int -> Int

6−double x = x * 2;

6+double x = x * 2

8−vec : (n ** Vect Int n);

8+vec : (n ** Vect Int n)

9−vec = (_ ** [3, 4]);

9+vec = (_ ** [3, 4])

11−list_lookup : Nat -> List a -> Maybe a;

11+list_lookup : Nat -> List a -> Maybe a

12−list_lookup _ Nil = Nothing;

12+list_lookup _ Nil = Nothing

13−list_lookup O (x :: xs) = Just x;

13+list_lookup O (x :: xs) = Just x

14−list_lookup (S k) (x :: xs) = list_lookup k xs;

14+list_lookup (S k) (x :: xs) = list_lookup k xs

16−lookup_default : Nat -> List a -> a -> a;

16+lookup_default : Nat -> List a -> a -> a

17lookup_default i xs def = case list_lookup i xs of {

18 Nothing => def

19 | Just x => x

20− };

20+ }

tutorial/examples/vbroken.idr+3−4

@@ -1,6 +1,5 @@

1−

2−vapp : Vect a n -> Vect a m -> Vect a (n + m);

1+vapp : Vect a n -> Vect a m -> Vect a (n + m)

3−vapp Nil ys = ys;

2+vapp Nil ys = ys

4−vapp (x :: xs) ys = x :: vapp xs xs; -- BROKEN

3+vapp (x :: xs) ys = x :: vapp xs xs -- BROKEN

tutorial/examples/views.idr+14−14

@@ -1,23 +1,23 @@

1−module views;

1+module views

3data Parity : Nat -> Set where

4 even : Parity (n + n)

5− | odd : Parity (S (n + n));

5+ | odd : Parity (S (n + n))

7−parity : (n:Nat) -> Parity n;

7+parity : (n:Nat) -> Parity n

8−parity O = even {n=O};

8+parity O = even {n=O}

9−parity (S O) = odd {n=O};

9+parity (S O) = odd {n=O}

10parity (S (S k)) with parity k {

11− parity (S (S (j + j))) | even ?= even {n=S j};

11+ parity (S (S (j + j))) | even ?= even {n=S j}

12− parity (S (S (S (j + j)))) | odd ?= odd {n=S j};

12+ parity (S (S (S (j + j)))) | odd ?= odd {n=S j}

13}

16−natToBin : Nat -> List Bool;

16+natToBin : Nat -> List Bool

17−natToBin O = Nil;

17+natToBin O = Nil

18natToBin k with parity k {

19− natToBin (j + j) | even = False :: natToBin j;

19+ natToBin (j + j) | even = False :: natToBin j

20− natToBin (S (j + j)) | odd = True :: natToBin j;

20+ natToBin (S (j + j)) | odd = True :: natToBin j

21}

@@ -28,13 +28,13 @@ views.parity_lemma_2 = proof {

28 intro;

29 rewrite plusn_Sm j j;

30 trivial;

31−};

31+}

33views.parity_lemma_1 = proof {

34− intro j;

34+ intro;

35 intro;

36 rewrite plusn_Sm j j;

37 trivial;

38−};

38+}

tutorial/idris-tutorial.pdf

Binary file not shown.

tutorial/interp.tex+38−38

@@ -9,7 +9,7 @@ language. We have integers, booleans, and functions, represented by \texttt{Ty}:

10\begin{SaveVerbatim}{tydecl}

12−data Ty = TyInt | TyBool | TyFun Ty Ty;

12+data Ty = TyInt | TyBool | TyFun Ty Ty

14\end{SaveVerbatim}

15\useverb{tydecl}

@@ -20,10 +20,10 @@ type:

21\begin{SaveVerbatim}{interpty}

23−interpTy : Ty -> Set;

23+interpTy : Ty -> Set

24−interpTy TyInt = Int;

24+interpTy TyInt = Int

25−interpTy TyBool = Bool;

25+interpTy TyBool = Bool

26−interpTy (TyFun A T) = interpTy A -> interpTy T;

26+interpTy (TyFun A T) = interpTy A -> interpTy T

28\end{SaveVerbatim}

29\useverb{interpty}

@@ -62,7 +62,7 @@ constructor in turn.

63data HasType : (i : Fin n) -> Vect Ty n -> Ty -> Set where

64 stop : HasType fO (t :: G) t

65− | pop : HasType k G t -> HasType (fS k) (u :: G) t;

65+ | pop : HasType k G t -> HasType (fS k) (u :: G) t

67data Expr : Vect Ty n -> Ty -> Set where

68 Var : HasType i G t -> Expr G t

@@ -71,7 +71,7 @@ data Expr : Vect Ty n -> Ty -> Set where

71 | App : Expr G (TyFun a t) -> Expr G a -> Expr G t

72 | Op : (interpTy a -> interpTy b -> interpTy c) -> Expr G a -> Expr G b ->

73 Expr G c

74− | If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a;

74+ | If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a

76\end{SaveVerbatim}

77\codefig{exprty}{Expression representation}

@@ -86,7 +86,7 @@ Variables are represented by a proof of their membership in the context,

87data HasType : (i : Fin n) -> Vect Ty n -> Ty -> Set where

88 stop : HasType fO (t :: G) t

89− | pop : HasType k G t -> HasType (fS k) (u :: G) t;

89+ | pop : HasType k G t -> HasType (fS k) (u :: G) t

91\end{SaveVerbatim}

92\useverb{hastype}

@@ -163,7 +163,7 @@ have the same type:

163

164\begin{SaveVerbatim}{ifcon}

165

166−If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a;

166+If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a

167

168\end{SaveVerbatim}

169\useverb{ifcon}

@@ -180,25 +180,25 @@ is defined in the context, we can then produce a value from the environment:

180

181data Env : Vect Ty n -> Set where

182 Nil : Env Nil

183− | (::) : interpTy a -> Env G -> Env (a :: G);

183+ | (::) : interpTy a -> Env G -> Env (a :: G)

184

185−lookup : HasType i G t -> Env G -> interpTy t;

185+lookup : HasType i G t -> Env G -> interpTy t

186−lookup stop (x :: xs) = x;

186+lookup stop (x :: xs) = x

187−lookup (pop k) (x :: xs) = lookup k xs;

187+lookup (pop k) (x :: xs) = lookup k xs

188

189\end{SaveVerbatim}

190\useverb{envtype}

191

192\begin{SaveVerbatim}{interpdef}

193

194−interp : Env G -> Expr G t -> interpTy t;

194+interp : Env G -> Expr G t -> interpTy t

195−interp env (Var i) = lookup i env;

195+interp env (Var i) = lookup i env

196−interp env (Val x) = x;

196+interp env (Val x) = x

197−interp env (Lam sc) = \x => interp (x :: env) sc;

197+interp env (Lam sc) = \x => interp (x :: env) sc

198−interp env (App f s) = (interp env f) (interp env s);

198+interp env (App f s) = (interp env f) (interp env s)

199−interp env (Op op x y) = op (interp env x) (interp env y);

199+interp env (Op op x y) = op (interp env x) (interp env y)

200interp env (If x t e) = if (interp env x) then (interp env t)

201− else (interp env e);

201+ else (interp env e)

202

203\end{SaveVerbatim}

204\codefig{interpdef}{Intepreter definition}

@@ -210,7 +210,7 @@ concrete \Idris{} value with respect to a specific environment:

210

211\begin{SaveVerbatim}{interpty}

212

213−interp : Env G -> Expr G t -> interpTy t;

213+interp : Env G -> Expr G t -> interpTy t

214

215\end{SaveVerbatim}

216\useverb{interpty}

@@ -220,7 +220,7 @@ To translate a variable, we simply look it up in the environment:

220

221\begin{SaveVerbatim}{varinterp}

222

223−interp env (Var i) = lookup i env;

223+interp env (Var i) = lookup i env

224

225\end{SaveVerbatim}

226\useverb{varinterp}

@@ -230,7 +230,7 @@ To translate a value, we just return the concrete representation of the value:

230

231\begin{SaveVerbatim}{valinterp}

232

233−interp env (Val x) = x;

233+interp env (Val x) = x

234

235\end{SaveVerbatim}

236\useverb{valinterp}

@@ -242,7 +242,7 @@ function in the object language is translated to an \Idris{} function:

242

243\begin{SaveVerbatim}{laminterp}

244

245−interp env (Lam sc) = \x => interp (x :: env) sc;

245+interp env (Lam sc) = \x => interp (x :: env) sc

246

247\end{SaveVerbatim}

248\useverb{laminterp}

@@ -254,7 +254,7 @@ type:

254

255\begin{SaveVerbatim}{appinterp}

256

257−interp env (App f s) = (interp env f) (interp env s);

257+interp env (App f s) = (interp env f) (interp env s)

258

259\end{SaveVerbatim}

260\useverb{appinterp}

@@ -267,9 +267,9 @@ directly.

267

268\begin{SaveVerbatim}{opinterp}

269

270−interp env (Op op x y) = op (interp env x) (interp env y);

270+interp env (Op op x y) = op (interp env x) (interp env y)

271interp env (If x t e) = if (interp env x) then (interp env t)

272− else (interp env e);

272+ else (interp env e)

273

274\end{SaveVerbatim}

275\useverb{opinterp}

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

280

281\begin{SaveVerbatim}{addtest}

282

283−add : Expr G (TyFun TyInt (TyFun TyInt TyInt));

283+add : Expr G (TyFun TyInt (TyFun TyInt TyInt))

284−add = Lam (Lam (Op (+) (Var stop) (Var (pop stop))));

284+add = Lam (Lam (Op (+) (Var stop) (Var (pop stop))))

285

286\end{SaveVerbatim}

287\useverb{addtest}

@@ -293,8 +293,8 @@ be evaluated if necessary:

293

294\begin{SaveVerbatim}{lazyapp}

295

296−app : |(f : Expr G (TyFun a t)) -> Expr G a -> Expr G t;

296+app : |(f : Expr G (TyFun a t)) -> Expr G a -> Expr G t

297−app = \f, a => App f a;

297+app = \f, a => App f a

298

299\end{SaveVerbatim}

300\useverb{lazyapp}

@@ -306,10 +306,10 @@ is written as follows:

306

307\begin{SaveVerbatim}{facttest}

308

309−fact : Expr G (TyFun TyInt TyInt);

309+fact : Expr G (TyFun TyInt TyInt)

310fact = Lam (If (Op (==) (Var stop) (Val 0))

311 (Val 1) (Op (*) (app fact (Op (-) (Var stop) (Val 1)))

312− (Var stop)));

312+ (Var stop)))

313

314\end{SaveVerbatim}

315\useverb{facttest}

@@ -319,11 +319,11 @@ on user input:

319

320\begin{SaveVerbatim}{factmain}

321

322−main : IO ();

322+main : IO ()

323−main = do { putStr "Enter a number: ";

323+main = do { putStr "Enter a number: "

324− x <- getLine;

324+ x <- getLine

325− print (interp [] fact (prim__strToInt x));

325+ print (interp [] fact (prim__strToInt x))

326− };

326+ }

327

328\end{SaveVerbatim}

329\useverb{factmain}

tutorial/intro.tex+1−1

@@ -33,7 +33,7 @@ to the \texttt{app} function, which concatenates vectors:

34\begin{SaveVerbatim}{appendv}

36−app : Vect a n -> Vect a m -> Vect a (n + m);

36+app : Vect a n -> Vect a m -> Vect a (n + m)

38\end{SaveVerbatim}

39\useverb{appendv}

tutorial/miscellany.tex+16−16

@@ -15,12 +15,12 @@ greater than sign \texttt{>}, for example:

16\begin{SaveVerbatim}{litidr}

18−> module literate;

18+> module literate

20This is a comment. The main program is below

22−> main : IO ();

22+> main : IO ()

23−> main = putStrLn "Hello literate world!\n";

23+> main = putStrLn "Hello literate world!\n"

25\end{SaveVerbatim}

26\useverb{litidr}

@@ -41,7 +41,7 @@ types we can handle:

42\begin{SaveVerbatim}{foreignty}

46\end{SaveVerbatim}

47\useverb{foreignty}

@@ -54,13 +54,13 @@ following function:

55\begin{SaveVerbatim}{interpfty}

57−interpFTy : FTy -> Set;

57+interpFTy : FTy -> Set

58−interpFTy FInt = Int;

58+interpFTy FInt = Int

59−interpFTy FFloat = Float;

59+interpFTy FFloat = Float

60−interpFTy FChar = Char;

60+interpFTy FChar = Char

61−interpFTy FString = String;

61+interpFTy FString = String

62−interpFTy FPtr = Ptr;

62+interpFTy FPtr = Ptr

63−interpFTy FUnit = ();

63+interpFTy FUnit = ()

65\end{SaveVerbatim}

66\useverb{interpfty}

@@ -71,7 +71,7 @@ can then be converted to an \Idris{} type:

72\begin{SaveVerbatim}{ffunty}

74−ForeignTy : (xs:List FTy) -> (t:FTy) -> Set;

74+ForeignTy : (xs:List FTy) -> (t:FTy) -> Set

76\end{SaveVerbatim}

77\useverb{ffunty}

@@ -100,9 +100,9 @@ converts this description to a function callable by \Idris{}

100

101data Foreign : Set -> Set where

102 FFun : String -> (xs:List FTy) -> (t:FTy) ->

103− Foreign (ForeignTy xs t);

103+ Foreign (ForeignTy xs t)

104

105−mkForeign : Foreign x -> x;

105+mkForeign : Foreign x -> x

106

107\end{SaveVerbatim}

108\useverb{mkForeign}

@@ -113,8 +113,8 @@ an external function \texttt{putStr} defined in the run-time system:

113

114\begin{SaveVerbatim}{putStrex}

115

116−putStr : String -> IO ();

116+putStr : String -> IO ()

117−putStr x = mkForeign (FFun "putStr" [FString] FUnit) x;

117+putStr x = mkForeign (FFun "putStr" [FString] FUnit) x

118\end{SaveVerbatim}

119\useverb{putStrex}

120

tutorial/modules.tex+33−33

@@ -12,37 +12,37 @@ tree type \texttt{BTree} (in a file \texttt{btree.idr}) and Figure

13\begin{SaveVerbatim}{bstmod}

15−module btree;

15+module btree

17data BTree a = Leaf

18− | Node (BTree a) a (BTree a);

18+ | Node (BTree a) a (BTree a)

20−insert : Ord a => a -> BTree a -> BTree a;

20+insert : Ord a => a -> BTree a -> BTree a

21−insert x Leaf = Node Leaf x Leaf;

21+insert x Leaf = Node Leaf x Leaf

22insert x (Node l v r) = if (x < v) then (Node (insert x l) v r)

23− else (Node l v (insert x r));

23+ else (Node l v (insert x r))

25−toList : BTree a -> List a;

25+toList : BTree a -> List a

26−toList Leaf = [];

26+toList Leaf = []

27−toList (Node l v r) = app (toList l) (v :: toList r);

27+toList (Node l v r) = app (toList l) (v :: toList r)

29−toTree : Ord a => List a -> BTree a;

29+toTree : Ord a => List a -> BTree a

30−toTree [] = Leaf;

30+toTree [] = Leaf

31−toTree (x :: xs) = insert x (toTree xs);

31+toTree (x :: xs) = insert x (toTree xs)

33\end{SaveVerbatim}

34\codefig{bstmod}{Binary Tree module}

36\begin{SaveVerbatim}{bstmain}

38−module main;

38+module main

40−import btree;

40+import btree

42−main : IO ();

42+main : IO ()

43−main = do { let t = toTree [1,8,2,7,9,3];

43+main = do { let t = toTree [1,8,2,7,9,3]

44− print (toList t);

44+ print (toList t)

45− };

45+ }

47\end{SaveVerbatim}

48\codefig{bstmain}{Binary Tree main program}

@@ -97,26 +97,26 @@ Figure \ref{bstmodp}.

98\begin{SaveVerbatim}{bstmodp}

100−module btree;

100+module btree

101

102abstract data BTree a = Leaf

103− | Node (BTree a) a (BTree a);

103+ | Node (BTree a) a (BTree a)

104

105abstract

106−insert : Ord a => a -> BTree a -> BTree a;

106+insert : Ord a => a -> BTree a -> BTree a

107−insert x Leaf = Node Leaf x Leaf;

107+insert x Leaf = Node Leaf x Leaf

108insert x (Node l v r) = if (x < v) then (Node (insert x l) v r)

109− else (Node l v (insert x r));

109+ else (Node l v (insert x r))

110

111abstract

112−toList : BTree a -> List a;

112+toList : BTree a -> List a

113−toList Leaf = [];

113+toList Leaf = []

114−toList (Node l v r) = app (toList l) (v :: toList r);

114+toList (Node l v r) = app (toList l) (v :: toList r)

115

116abstract

117−toTree : Ord a => List a -> BTree a;

117+toTree : Ord a => List a -> BTree a

118−toTree [] = Leaf;

118+toTree [] = Leaf

119−toTree (x :: xs) = insert x (toTree xs);

119+toTree (x :: xs) = insert x (toTree xs)

120

121\end{SaveVerbatim}

122\codefig{bstmodp}{Binary Tree module, with export modifiers}

@@ -144,16 +144,16 @@ the same module:

144

145\begin{SaveVerbatim}{nsfoo}

146

147−module foo;

147+module foo

148

149namespace x {

150− test : Int -> Int;

150+ test : Int -> Int

151− test x = x * 2;

151+ test x = x * 2

152}

153

154namespace y {

155− test : String -> String;

155+ test : String -> String

156− test x = x ++ x;

156+ test x = x ++ x

157}

158

159\end{SaveVerbatim}

tutorial/provisional.tex+32−32

@@ -9,9 +9,9 @@ example, recall the \texttt{parity} function:

10data Parity : Nat -> Set where

11 even : Parity (n + n)

12− | odd : Parity (S (n + n));

12+ | odd : Parity (S (n + n))

14−parity : (n:Nat) -> Parity n;

14+parity : (n:Nat) -> Parity n

16\end{SaveVerbatim}

17\useverb{pardecl}

@@ -21,12 +21,12 @@ We'd like to implement this as follows:

22\begin{SaveVerbatim}{parfail}

24−parity : (n:Nat) -> Parity n;

24+parity : (n:Nat) -> Parity n

25−parity O = even {n=O};

25+parity O = even {n=O}

26−parity (S O) = odd {n=O};

26+parity (S O) = odd {n=O}

27parity (S (S k)) with parity k {

28− parity (S (S (j + j))) | even = even {n=S j};

28+ parity (S (S (j + j))) | even = even {n=S j}

29− parity (S (S (S (j + j)))) | odd = odd {n=S j};

29+ parity (S (S (S (j + j)))) | odd = odd {n=S j}

30}

32\end{SaveVerbatim}

@@ -77,12 +77,12 @@ except that they introduce the right hand side with a \texttt{?=} rathar than

78\begin{SaveVerbatim}{paritypro}

80−parity : (n:Nat) -> Parity n;

80+parity : (n:Nat) -> Parity n

81−parity O = even {n=O};

81+parity O = even {n=O}

82−parity (S O) = odd {n=O};

82+parity (S O) = odd {n=O}

83parity (S (S k)) with parity k {

84− parity (S (S (j + j))) | even ?= even {n=S j};

84+ parity (S (S (j + j))) | even ?= even {n=S j}

85− parity (S (S (S (j + j)))) | odd ?= odd {n=S j};

85+ parity (S (S (S (j + j)))) | odd ?= odd {n=S j}

86}

88\end{SaveVerbatim}

@@ -128,7 +128,7 @@ the prelude:

128

129\begin{SaveVerbatim}{plusnsm}

130

131−plusn_Sm : (n : Nat) -> (m : Nat) -> (plus n (S m)) = S (plus n m);

131+plusn_Sm : (n : Nat) -> (m : Nat) -> (plus n (S m)) = S (plus n m)

132

133\end{SaveVerbatim}

134\useverb{plusnsm}

@@ -182,7 +182,7 @@ a value of the incorrect types:

182

183\begin{SaveVerbatim}{believe}

184

185−believe_me : a -> b;

185+believe_me : a -> b

186

187\end{SaveVerbatim}

188\useverb{believe}

@@ -198,7 +198,7 @@ views.parity_lemma_2 = proof {

198 intro;

199 intro;

200 exact believe_me value;

201−};

201+}

202

203\end{SaveVerbatim}

204\useverb{pladodgy}

@@ -221,7 +221,7 @@ case \texttt{Nat}):

221data Binary : Nat -> Set where

222 bEnd : Binary O

223 | bO : Binary n -> Binary (n + n)

224− | bI : Binary n -> Binary (S (n + n));

224+ | bI : Binary n -> Binary (S (n + n))

225

226\end{SaveVerbatim}

227\useverb{bindef}

@@ -238,7 +238,7 @@ resulting binary number is a faithful representation of the original Nat:

238

239\begin{SaveVerbatim}{ntbty}

240

241−natToBin : (n:Nat) -> Binary n;

241+natToBin : (n:Nat) -> Binary n

242

243\end{SaveVerbatim}

244\useverb{ntbty}

@@ -250,11 +250,11 @@ provisional definition in the odd case:

250

251\begin{SaveVerbatim}{ntbdef}

252

253−natToBin : (n:Nat) -> Binary n;

253+natToBin : (n:Nat) -> Binary n

254−natToBin O = bEnd;

254+natToBin O = bEnd

255natToBin (S k) with parity k {

256− natToBin (S (j + j)) | even = bI (natToBin j);

256+ natToBin (S (j + j)) | even = bI (natToBin j)

257− natToBin (S (S (j + j))) | odd ?= bO (natToBin (S j));

257+ natToBin (S (S (j + j))) | odd ?= bO (natToBin (S j))

258}

259

260\end{SaveVerbatim}

@@ -271,7 +271,7 @@ natToBin_lemma_1 = proof {

271 intro;

272 rewrite plusn_Sm j j;

273 trivial;

274−};

274+}

275

276\end{SaveVerbatim}

277\useverb{ntboddprf}

@@ -282,13 +282,13 @@ outputs it in binary.

282

283\begin{SaveVerbatim}{binmain}

284

285−main : IO ();

285+main : IO ()

286−main = do { putStr "Enter a number: ";

286+main = do { putStr "Enter a number: "

287− x <- getLine;

287+ x <- getLine

288− let n = prim__strToInt x;

288+ let n = prim__strToInt x

289− let b = natToBin (fromInteger n);

289+ let b = natToBin (fromInteger n)

290− print b;

290+ print b

291− };

291+ }

292

293\end{SaveVerbatim}

294\useverb{binmain}

@@ -299,9 +299,9 @@ For this to work, of course, we need a \texttt{Show} instance for \texttt{Binary

299\begin{SaveVerbatim}{showbin}

300

301instance Show (Binary n) where {

302− show (bO x) = show x ++ "0";

302+ show (bO x) = show x ++ "0"

303− show (bI x) = show x ++ "1";

303+ show (bI x) = show x ++ "1"

304− show bEnd = "";

304+ show bEnd = ""

305}

306

307\end{SaveVerbatim}

tutorial/starting.tex+3−3

@@ -41,10 +41,10 @@ text:

42\begin{SaveVerbatim}{hello}

44−module main;

44+module main

46−main : IO();

46+main : IO ()

47−main = putStrLn "Hello world";

47+main = putStrLn "Hello world"

49\end{SaveVerbatim}

50\useverb{hello}

tutorial/theorems.tex+19−19

@@ -9,7 +9,7 @@ the following definition:

9\begin{SaveVerbatim}{}

11data (=) : a -> b -> Set where

12− refl : x = x;

12+ refl : x = x

14\end{SaveVerbatim}

15\useverb{}

@@ -20,11 +20,11 @@ construct a proof of equality is if values actually are equal. For example:

21\begin{SaveVerbatim}{eqprf}

23−fiveIsFive : 5 = 5;

23+fiveIsFive : 5 = 5

24−fiveIsFive = refl;

24+fiveIsFive = refl

26−twoPlusTwo : 2 + 2 = 4;

26+twoPlusTwo : 2 + 2 = 4

27−twoPlusTwo = refl;

27+twoPlusTwo = refl

29\end{SaveVerbatim}

30\useverb{eqprf}

@@ -36,7 +36,7 @@ we want to prove the following theorem about the reduction behaviour of \texttt{

37\begin{SaveVerbatim}{plusred}

39−plusReduces : (n:Nat) -> plus O n = n;

39+plusReduces : (n:Nat) -> plus O n = n

41\end{SaveVerbatim}

42\useverb{plusred}

@@ -55,7 +55,7 @@ by the definition of \texttt{plus}:

56\begin{SaveVerbatim}{plusredp}

58−plusReduces n = refl;

58+plusReduces n = refl

60\end{SaveVerbatim}

61\useverb{plusredp}

@@ -67,9 +67,9 @@ on the first argument to \texttt{plus}, namely \texttt{n}.

68\begin{SaveVerbatim}{plusRedO}

70−plusReducesO : (n:Nat) -> n = plus n O;

70+plusReducesO : (n:Nat) -> n = plus n O

71−plusReducesO O = refl;

71+plusReducesO O = refl

72−plusReducesO (S k) = eqRespS (plusReducesO k);

72+plusReducesO (S k) = eqRespS (plusReducesO k)

74\end{SaveVerbatim}

75\useverb{plusRedO}

@@ -80,7 +80,7 @@ equality respects successor:

81\begin{SaveVerbatim}{resps}

83−eqRespS : m = n -> S m = S n;

83+eqRespS : m = n -> S m = S n

85\end{SaveVerbatim}

86\useverb{resps}

@@ -90,9 +90,9 @@ We can do the same for the reduction behaviour of plus on successors:

91\begin{SaveVerbatim}{plusRedS}

93−plusReducesS : (n:Nat) -> (m:Nat) -> S (plus n m) = plus n (S m);

93+plusReducesS : (n:Nat) -> (m:Nat) -> S (plus n m) = plus n (S m)

94−plusReducesS O m = refl;

94+plusReducesS O m = refl

95−plusReducesS (S k) m = eqRespS (plusReducesS k m);

95+plusReducesS (S k) m = eqRespS (plusReducesS k m)

97\end{SaveVerbatim}

98\useverb{plusRedS}

@@ -114,10 +114,10 @@ hypothesis, and insert \emph{metavariables} for the rest of the definition:

114

115\begin{SaveVerbatim}{prOstruct}

116

117−plusReducesO' : (n:Nat) -> n = plus n O;

117+plusReducesO' : (n:Nat) -> n = plus n O

118−plusReducesO' O = ?plusredO_O;

118+plusReducesO' O = ?plusredO_O

119plusReducesO' (S k) = let ih = plusReducesO' k in

120− ?plusredO_S;

120+ ?plusredO_S

121

122\end{SaveVerbatim}

123\useverb{prOstruct}

@@ -208,7 +208,7 @@ This also outputs a trace of the proof:

208plusredO_O = proof {

209 compute;

210 refine refl;

211−};

211+}

212

213\end{SaveVerbatim}

214\useverb{prOprooftrace}

@@ -286,7 +286,7 @@ plusredO_S = proof {

286 intro;

287 rewrite ih;

288 trivial;

289−};

289+}

290

291\end{SaveVerbatim}

292\useverb{prOStrace}

tutorial/typesfuns.tex+111−109

@@ -13,19 +13,19 @@ environment by typing \texttt{idris prims.idr}:

14\begin{SaveVerbatim}{constprims}

16−module prims;

16+module prims

18−x : Int;

18+x : Int

19−x = 42;

19+x = 42

21−foo : String;

21+foo : String

22−foo = "Sausage machine";

22+foo = "Sausage machine"

24−bar : Char;

24+bar : Char

25−bar = 'Z';

25+bar = 'Z'

27−quux : Bool;

27+quux : Bool

28−quux = False;

28+quux = False

30\end{SaveVerbatim}

31\useverb{constprims}

@@ -35,8 +35,10 @@ An \Idris{} file consists of an optional module declaration (here

35however \Idris{} programs can consist of several modules, and the definitions

36in each module each have their own namespace, as we will discuss shortly) and a

37collection of declarations and definitions. Each definition must have a type

38−declaration (here, \texttt{x : Int}, \texttt{foo : String}, etc). Each

38+declaration (here, \texttt{x : Int}, \texttt{foo : String}, etc).

39−component is separated by a semi-colon.

39+Indentation is significant --- a new declaration begins at the same leve

40+of indentation as the preceding declaration. Alternatively, declarations

41+may be terminated with a semicolon.

41A library module \texttt{prelude} is automatically imported by every \Idris{} program,

43A library module \texttt{prelude} is automatically imported by every \Idris{} program,

42including facilities for IO, arithmetic, data structures and various common

44including facilities for IO, arithmetic, data structures and various common

@@ -76,9 +78,9 @@ example, can be declared as follows:

77\begin{SaveVerbatim}{natlist}

79\begin{SaveVerbatim}{natlist}

79−data Nat = O | S Nat; -- Natural numbers

81+data Nat = O | S Nat -- Natural numbers

80− -- (zero and successor)

82+ -- (zero and successor)

81−data List a = Nil | (::) a (List a); -- Polymorphic lists

83+data List a = Nil | (::) a (List a) -- Polymorphic lists

83\end{SaveVerbatim}

85\end{SaveVerbatim}

84\useverb{natlist}

86\useverb{natlist}

@@ -93,7 +95,7 @@ such as this can be added using a fixity declaration, as follows:

94\begin{SaveVerbatim}{infixcons}

96\begin{SaveVerbatim}{infixcons}

96−infixr 7 :: ;

98+infixr 7 ::

98\end{SaveVerbatim}

100\end{SaveVerbatim}

99\useverb{infixcons}

101\useverb{infixcons}

@@ -124,14 +126,14 @@ defined as follows, again taken from the standard library:

124\begin{SaveVerbatim}{natfns}

126\begin{SaveVerbatim}{natfns}

125

127

126-- Unary addition

128-- Unary addition

127−plus : Nat -> Nat -> Nat;

129+plus : Nat -> Nat -> Nat

128−plus O y = y;

130+plus O y = y

129−plus (S k) y = S (plus k y);

131+plus (S k) y = S (plus k y)

130

132

131-- Unary multiplication

133-- Unary multiplication

132−mult : Nat -> Nat -> Nat;

134+mult : Nat -> Nat -> Nat

133−mult O y = O;

135+mult O y = O

134−mult (S k) y = plus y (mult k y);

136+mult (S k) y = plus y (mult k y)

135

137

136\end{SaveVerbatim}

138\end{SaveVerbatim}

137\useverb{natfns}

139\useverb{natfns}

@@ -186,11 +188,11 @@ accumulates the new, reversed list, and which does not need to be visible global

186

188

187\begin{SaveVerbatim}{revwhere}

189\begin{SaveVerbatim}{revwhere}

188

190

189−rev : List a -> List a;

191+rev : List a -> List a

190rev xs = revAcc [] xs where {

192rev xs = revAcc [] xs where {

191− revAcc : List a -> List a -> List a;

193+ revAcc : List a -> List a -> List a

192− revAcc acc [] = acc;

194+ revAcc acc [] = acc

193− revAcc acc (x :: xs) = revAcc (x :: acc) xs;

195+ revAcc acc (x :: xs) = revAcc (x :: acc) xs

194}

196}

195

197

196\end{SaveVerbatim}

198\end{SaveVerbatim}

@@ -207,9 +209,9 @@ behaviour, the \texttt{a} can be brought into scope as follows:

207

209

208\begin{SaveVerbatim}{revwhereb}

210\begin{SaveVerbatim}{revwhereb}

209

211

210−rev : List a -> List a;

212+rev : List a -> List a

211rev {a} xs = revAcc [] xs where {

213rev {a} xs = revAcc [] xs where {

212− revAcc : List a -> List a -> List a;

214+ revAcc : List a -> List a -> List a

213 ...

215 ...

214}

216}

215

217

@@ -228,7 +230,7 @@ we declare vectors as follows:

228

230

229data Vect : Set -> Nat -> Set where

231data Vect : Set -> Nat -> Set where

230 Nil : Vect a O

232 Nil : Vect a O

231− | (::) : a -> Vect a k -> Vect a (S k);

233+ | (::) : a -> Vect a k -> Vect a (S k)

232

234

233\end{SaveVerbatim}

235\end{SaveVerbatim}

234\useverb{vect}

236\useverb{vect}

@@ -257,9 +259,9 @@ library, appends two \tTC{Vect}s:

257

259

258\begin{SaveVerbatim}{vapp}

260\begin{SaveVerbatim}{vapp}

259

261

260−app : Vect A n -> Vect A m -> Vect A (n + m);

262+app : Vect A n -> Vect A m -> Vect A (n + m)

261−app Nil ys = ys;

263+app Nil ys = ys

262−app (x :: xs) ys = x :: app xs ys;

264+app (x :: xs) ys = x :: app xs ys

263

265

264\end{SaveVerbatim}

266\end{SaveVerbatim}

265\useverb{vapp}

267\useverb{vapp}

@@ -270,9 +272,9 @@ not hold, \Idris{} will not accept the definition. For example:

270

272

271\begin{SaveVerbatim}{vapperr}

273\begin{SaveVerbatim}{vapperr}

272

274

273−app : Vect a n -> Vect a m -> Vect a (n + m);

275+app : Vect a n -> Vect a m -> Vect a (n + m)

274−app Nil ys = ys;

276+app Nil ys = ys

275−app (x :: xs) ys = x :: app xs xs; -- BROKEN

277+app (x :: xs) ys = x :: app xs xs -- BROKEN

276

278

277\end{SaveVerbatim}

279\end{SaveVerbatim}

278\useverb{vapperr}

280\useverb{vapperr}

@@ -303,7 +305,7 @@ They are declared as follows (again, in the prelude):

303

305

304data Fin : Nat -> Set where

306data Fin : Nat -> Set where

305 fO : Fin (S k)

307 fO : Fin (S k)

306− | fS : Fin k -> Fin (S k);

308+ | fS : Fin k -> Fin (S k)

307

309

308\end{SaveVerbatim}

310\end{SaveVerbatim}

309\useverb{findecl}

311\useverb{findecl}

@@ -321,9 +323,9 @@ is defined in the prelude:

321

323

322\begin{SaveVerbatim}{vlookup}

324\begin{SaveVerbatim}{vlookup}

323

325

324−lookup : Fin n -> Vect a n -> a;

326+lookup : Fin n -> Vect a n -> a

325−lookup fO (x :: xs) = x;

327+lookup fO (x :: xs) = x

326−lookup (fS k) (x :: xs) = lookup k xs;

328+lookup (fS k) (x :: xs) = lookup k xs

327

329

328\end{SaveVerbatim}

330\end{SaveVerbatim}

329\useverb{vlookup}

331\useverb{vlookup}

@@ -384,7 +386,7 @@ declared the type of \texttt{lookup} as:

384

386

385\begin{SaveVerbatim}{vlookupn}

387\begin{SaveVerbatim}{vlookupn}

386

388

387−lookup : (i:Fin n) -> (xs:Vect a n) -> a;

389+lookup : (i:Fin n) -> (xs:Vect a n) -> a

388

390

389\end{SaveVerbatim}

391\end{SaveVerbatim}

390\useverb{vlookupn}

392\useverb{vlookupn}

@@ -406,7 +408,7 @@ definition, which defines a predicate on vectors:

406

408

407data Elem : a -> (Vect a n) -> Set where

409data Elem : a -> (Vect a n) -> Set where

408 here : {x:a} -> {xs:Vect a n} -> Elem x (x :: xs)

410 here : {x:a} -> {xs:Vect a n} -> Elem x (x :: xs)

409− | there : {x,y:a} -> {xs:Vect a n} -> Elem x xs -> Elem x (y :: xs);

411+ | there : {x,y:a} -> {xs:Vect a n} -> Elem x xs -> Elem x (y :: xs)

410

412

411\end{SaveVerbatim}

413\end{SaveVerbatim}

412\useverb{elem}

414\useverb{elem}

@@ -419,11 +421,11 @@ or \texttt{there}, in the tail of the vector. For example:

419

421

420\begin{SaveVerbatim}{testelem}

422\begin{SaveVerbatim}{testelem}

421

423

422−testVec : Vect Int 4;

424+testVec : Vect Int 4

423−testVec = 3 :: 4 :: 5 :: 6 :: VNil;

425+testVec = 3 :: 4 :: 5 :: 6 :: VNil

424

426

425−inVect : Elem 5 testVec;

427+inVect : Elem 5 testVec

426−inVect = there (there here);

428+inVect = there (there here)

427

429

428\end{SaveVerbatim}

430\end{SaveVerbatim}

429\useverb{testelem}

431\useverb{testelem}

@@ -438,7 +440,7 @@ ordering of any implicit arguments which can appear within the block:

438using (x:a, y:a, xs:Vect a n) {

440using (x:a, y:a, xs:Vect a n) {

439 data Elem : a -> (Vect a n) -> Set where

441 data Elem : a -> (Vect a n) -> Set where

440 here : Elem x (x :: xs)

442 here : Elem x (x :: xs)

441− | there : Elem x xs -> Elem x (y :: xs);

443+ | there : Elem x xs -> Elem x (y :: xs)

442}

444}

443

445

444\end{SaveVerbatim}

446\end{SaveVerbatim}

@@ -454,7 +456,7 @@ encapsulated in the type \texttt{IO}:

454

456

455\begin{SaveVerbatim}{ioty}

457\begin{SaveVerbatim}{ioty}

456

458

457−data IO a; -- IO operation returning a value of type a

459+data IO a -- IO operation returning a value of type a

458

460

459\end{SaveVerbatim}

461\end{SaveVerbatim}

460\useverb{ioty}

462\useverb{ioty}

@@ -467,8 +469,8 @@ program:

467

469

468\begin{SaveVerbatim}{main}

470\begin{SaveVerbatim}{main}

469

471

470−main : IO ();

472+main : IO ()

471−main = putStrLn "Hello world";

473+main = putStrLn "Hello world"

472

474

473\end{SaveVerbatim}

475\end{SaveVerbatim}

474\useverb{main}

476\useverb{main}

@@ -479,8 +481,8 @@ outputs a string without a newline:

479

481

480\begin{SaveVerbatim}{putstr}

482\begin{SaveVerbatim}{putstr}

481

483

482−putStrLn : String -> IO ();

484+putStrLn : String -> IO ()

483−putStr : String -> IO ();

485+putStr : String -> IO ()

484

486

485\end{SaveVerbatim}

487\end{SaveVerbatim}

486

488

@@ -488,7 +490,7 @@ We can also read strings from user input:

488

490

489\begin{SaveVerbatim}{getline}

491\begin{SaveVerbatim}{getline}

490

492

491−getLine : IO String;

493+getLine : IO String

492

494

493\end{SaveVerbatim}

495\end{SaveVerbatim}

494\useverb{getline}

496\useverb{getline}

@@ -499,17 +501,17 @@ writing files, including:

499

501

500\begin{SaveVerbatim}{fileops}

502\begin{SaveVerbatim}{fileops}

501

503

502−data File; -- abstract

504+data File -- abstract

503−data Mode = Read | Write | ReadWrite;

505+data Mode = Read | Write | ReadWrite

504

506

505−openFile : String -> Mode -> IO File;

507+openFile : String -> Mode -> IO File

506−closeFile : File -> IO ();

508+closeFile : File -> IO ()

507

509

508−fread : File -> IO String;

510+fread : File -> IO String

509−fwrite : File -> String -> IO ();

511+fwrite : File -> String -> IO ()

510−feof : File -> IO Bool;

512+feof : File -> IO Bool

511

513

512−readFile : String -> IO String;

514+readFile : String -> IO String

513

515

514\end{SaveVerbatim}

516\end{SaveVerbatim}

515\useverb{fileops}

517\useverb{fileops}

@@ -525,11 +527,11 @@ operations with \texttt{do} notation:

525

527

526\begin{SaveVerbatim}{greet}

528\begin{SaveVerbatim}{greet}

527

529

528−greet : IO ();

530+greet : IO ()

529−greet = do { putStr "What is your name? ";

531+greet = do { putStr "What is your name? "

530− name <- getLine;

532+ name <- getLine

531− putStrLn ("Hello " ++ name);

533+ putStrLn ("Hello " ++ name)

532− };

534+ }

533

535

534\end{SaveVerbatim}

536\end{SaveVerbatim}

535\useverb{greet}

537\useverb{greet}

@@ -544,7 +546,7 @@ operation:

544

546

545\begin{SaveVerbatim}{return}

547\begin{SaveVerbatim}{return}

546

548

547−return : a -> IO a;

549+return : a -> IO a

548

550

549\end{SaveVerbatim}

551\end{SaveVerbatim}

550\useverb{return}

552\useverb{return}

@@ -566,11 +568,11 @@ We have already seen the \texttt{List} and \texttt{Vect} data types:

566

568

567\begin{SaveVerbatim}{listvec}

569\begin{SaveVerbatim}{listvec}

568

570

569−data List a = Nil | (::) a (List a);

571+data List a = Nil | (::) a (List a)

570

572

571data Vect : Set -> Nat -> Set where

573data Vect : Set -> Nat -> Set where

572 Nil : Vect a O

574 Nil : Vect a O

573− | (::) : a -> Vect a k -> Vect a (S k);

575+ | (::) : a -> Vect a k -> Vect a (S k)

574

576

575\end{SaveVerbatim}

577\end{SaveVerbatim}

576\useverb{listvec}

578\useverb{listvec}

@@ -594,13 +596,13 @@ and applies a function to every element of the list or vector.

594

596

595\begin{SaveVerbatim}{map}

597\begin{SaveVerbatim}{map}

596

598

597−map : (a -> b) -> List a -> List b;

599+map : (a -> b) -> List a -> List b

598−map f [] = [];

600+map f [] = []

599−map f (x :: xs) = f x :: map f xs;

601+map f (x :: xs) = f x :: map f xs

600

602

601−map : (a -> b) -> Vect a n -> Vect b n;

603+map : (a -> b) -> Vect a n -> Vect b n

602−map f [] = [];

604+map f [] = []

603−map f (x :: xs) = f x :: map f xs;

605+map f (x :: xs) = f x :: map f xs

604

606

605\end{SaveVerbatim}

607\end{SaveVerbatim}

606\useverb{map}

608\useverb{map}

@@ -610,11 +612,11 @@ For example, to double every element in a vector of integers:

610

612

611\begin{SaveVerbatim}{dvect}

613\begin{SaveVerbatim}{dvect}

612

614

613−intVec : Vect Int 5;

615+intVec : Vect Int 5

614−intVec = [1, 2, 3, 4, 5];

616+intVec = [1, 2, 3, 4, 5]

615

617

616−double : Int -> Int;

618+double : Int -> Int

617−double x = x * 2;

619+double x = x * 2

618

620

619\end{SaveVerbatim}

621\end{SaveVerbatim}

620\useverb{dvect}

622\useverb{dvect}

@@ -679,7 +681,7 @@ or there isn't:

679

681

680\begin{SaveVerbatim}{maybe}

682\begin{SaveVerbatim}{maybe}

681

683

682−data Maybe a = Just a | Nothing;

684+data Maybe a = Just a | Nothing

683

685

684\end{SaveVerbatim}

686\end{SaveVerbatim}

685\useverb{maybe}

687\useverb{maybe}

@@ -691,10 +693,10 @@ bounds error:

691

693

692\begin{SaveVerbatim}{lookuplist}

694\begin{SaveVerbatim}{lookuplist}

693

695

694−list_lookup : Nat -> List a -> Maybe a;

696+list_lookup : Nat -> List a -> Maybe a

695−list_lookup _ Nil = Nothing;

697+list_lookup _ Nil = Nothing

696−list_lookup O (x :: xs) = Just x;

698+list_lookup O (x :: xs) = Just x

697−list_lookup (S k) (x :: xs) = list_lookup k xs;

699+list_lookup (S k) (x :: xs) = list_lookup k xs

698

700

699\end{SaveVerbatim}

701\end{SaveVerbatim}

700\useverb{lookuplist}

702\useverb{lookuplist}

@@ -705,7 +707,7 @@ either by applying a function to the value, if there is one, or by providing a d

705

707

706\begin{SaveVerbatim}{maybefn}

708\begin{SaveVerbatim}{maybefn}

707

709

708−maybe : Maybe a -> |(default:b) -> (a -> b) -> b;

710+maybe : Maybe a -> |(default:b) -> (a -> b) -> b

709

711

710\end{SaveVerbatim}

712\end{SaveVerbatim}

711\useverb{maybefn}

713\useverb{maybefn}

@@ -724,7 +726,7 @@ Values can be paired with the following built-in data type:

724

726

725\begin{SaveVerbatim}{mkpair}

727\begin{SaveVerbatim}{mkpair}

726

728

727−data Pair a b = MkPair a b;

729+data Pair a b = MkPair a b

728

730

729\end{SaveVerbatim}

731\end{SaveVerbatim}

730\useverb{mkpair}

732\useverb{mkpair}

@@ -736,11 +738,11 @@ Tuples can contain an arbitrary number of values, represented as nested pairs:

736

738

737\begin{SaveVerbatim}{tuple}

739\begin{SaveVerbatim}{tuple}

738

740

739−fred : (String, Int);

741+fred : (String, Int)

740−fred = ("Fred", 42);

742+fred = ("Fred", 42)

741

743

742−jim : (String, Int, String);

744+jim : (String, Int, String)

743−jim = ("Jim", 25, "Cambridge");

745+jim = ("Jim", 25, "Cambridge")

744

746

745\end{SaveVerbatim}

747\end{SaveVerbatim}

746\useverb{tuple}

748\useverb{tuple}

@@ -753,7 +755,7 @@ the value of the first element:

753\begin{SaveVerbatim}{sigma}

755\begin{SaveVerbatim}{sigma}

754

756

755data Exists : (A : Set) -> (P : A -> Set) -> Set where

757data Exists : (A : Set) -> (P : A -> Set) -> Set where

756− Ex_intro : {P : A -> Set} -> (a : A) -> P a -> Exists A P;

758+ Ex_intro : {P : A -> Set} -> (a : A) -> P a -> Exists A P

757

759

758\end{SaveVerbatim}

760\end{SaveVerbatim}

759\useverb{sigma}

761\useverb{sigma}

@@ -766,8 +768,8 @@ constructs a value of this type. For example, we can pair a number with a

766

768

767\begin{SaveVerbatim}{dvec}

769\begin{SaveVerbatim}{dvec}

768

770

769−vec : (n : Nat ** Vect Int n);

771+vec : (n : Nat ** Vect Int n)

770−vec = (2 ** [3, 4]);

772+vec = (2 ** [3, 4])

771

773

772\end{SaveVerbatim}

774\end{SaveVerbatim}

773\useverb{dvec}

775\useverb{dvec}

@@ -780,8 +782,8 @@ written as:

780

782

781\begin{SaveVerbatim}{dvec1}

783\begin{SaveVerbatim}{dvec1}

782

784

783−vec : (n : Nat ** Vect Int n);

785+vec : (n : Nat ** Vect Int n)

784−vec = (_ ** [3, 4]);

786+vec = (_ ** [3, 4])

785

787

786\end{SaveVerbatim}

788\end{SaveVerbatim}

787\useverb{dvec1}

789\useverb{dvec1}

@@ -792,8 +794,8 @@ again, it can be inferred:

792

794

793\begin{SaveVerbatim}{dvec2}

795\begin{SaveVerbatim}{dvec2}

794

796

795−vec : (n ** Vect Int n);

797+vec : (n ** Vect Int n)

796−vec = (_ ** [3, 4]);

798+vec = (_ ** [3, 4])

797

799

798\end{SaveVerbatim}

800\end{SaveVerbatim}

799\useverb{dvec2}

801\useverb{dvec2}

@@ -806,7 +808,7 @@ length of the resulting vector will be:

806

808

807\begin{SaveVerbatim}{vfilter}

809\begin{SaveVerbatim}{vfilter}

808

810

809−filter : (a -> Bool) -> Vect a n -> (p ** Vect a p);

811+filter : (a -> Bool) -> Vect a n -> (p ** Vect a p)

810

812

811\end{SaveVerbatim}

813\end{SaveVerbatim}

812\useverb{vfilter}

814\useverb{vfilter}

@@ -816,7 +818,7 @@ If the \texttt{Vect} is empty, the result is easy:

816

818

817\begin{SaveVerbatim}{vfilternil}

819\begin{SaveVerbatim}{vfilternil}

818

820

819−vfilter p VNil = (_ , []);

821+vfilter p VNil = (_ , [])

820

822

821\end{SaveVerbatim}

823\end{SaveVerbatim}

822\useverb{vfilternil}

824\useverb{vfilternil}

@@ -830,7 +832,7 @@ notation. with allows pattern matching on intermediate values:

830\begin{SaveVerbatim}{vfiltercons}

832\begin{SaveVerbatim}{vfiltercons}

831

833

832filter p (x :: xs) with filter p xs {

834filter p (x :: xs) with filter p xs {

833− | (_ , xs') = if (p x) then (_ , x :: xs') else (_ , xs');

835+ | (_ , xs') = if (p x) then (_ , x :: xs') else (_ , xs')

834}

836}

835

837

836\end{SaveVerbatim}

838\end{SaveVerbatim}

@@ -847,9 +849,9 @@ Intermediate values can be calculated using \texttt{let} bindings:

847

849

848\begin{SaveVerbatim}{letb}

850\begin{SaveVerbatim}{letb}

849

851

850−mirror : List a -> List a;

852+mirror : List a -> List a

851mirror xs = let xs' = rev xs in

853mirror xs = let xs' = rev xs in

852− app xs xs';

854+ app xs xs'

853

855

854\end{SaveVerbatim}

856\end{SaveVerbatim}

855\useverb{letb}

857\useverb{letb}

@@ -860,11 +862,11 @@ fields from a record as follows, as well as by pattern matching at the top level

860

862

861\begin{SaveVerbatim}{letp}

863\begin{SaveVerbatim}{letp}

862

864

863−data Person = MkPerson String Int;

865+data Person = MkPerson String Int

864

866

865−showPerson : Person -> String;

867+showPerson : Person -> String

866showPerson p = let MkPerson name age = p in

868showPerson p = let MkPerson name age = p in

867− name ++ " is " ++ show age ++ " years old";

869+ name ++ " is " ++ show age ++ " years old"

868

870

869\end{SaveVerbatim}

871\end{SaveVerbatim}

870\useverb{letp}

872\useverb{letp}

@@ -891,9 +893,9 @@ follows:

891

893

892\begin{SaveVerbatim}{triples}

894\begin{SaveVerbatim}{triples}

893

895

894−pythag : Int -> List (Int, Int, Int);

896+pythag : Int -> List (Int, Int, Int)

895pythag n = [ (x, y, z) | z <- [1..n], y <- [1..z], x <- [1..y],

897pythag n = [ (x, y, z) | z <- [1..n], y <- [1..z], x <- [1..y],

896− x*x + y*y == z*z ];

898+ x*x + y*y == z*z ]

897

899

898\end{SaveVerbatim}

900\end{SaveVerbatim}

899\useverb{triples}

901\useverb{triples}

@@ -913,10 +915,10 @@ The following function, for example, splits a string into two at a given charact

913

915

914\begin{SaveVerbatim}{split}

916\begin{SaveVerbatim}{split}

915

917

916−splitAt : Char -> String -> (String, String);

918+splitAt : Char -> String -> (String, String)

917splitAt c x = case break (== c) x of {

919splitAt c x = case break (== c) x of {

918 (x, y) => (x, strTail y)

920 (x, y) => (x, strTail y)

919− };

921+ }

920

922

921\end{SaveVerbatim}

923\end{SaveVerbatim}

922\useverb{split}

924\useverb{split}

@@ -934,11 +936,11 @@ looks up an index and returns a default value if the index is out of bounds:

934

936

935\begin{SaveVerbatim}{listlookup}

937\begin{SaveVerbatim}{listlookup}

936

938

937−lookup_default : Nat -> List a -> a -> a;

939+lookup_default : Nat -> List a -> a -> a

938lookup_default i xs def = case list_lookup i xs of {

940lookup_default i xs def = case list_lookup i xs of {

939 Nothing => def

941 Nothing => def

940 | Just x => x

942 | Just x => x

941− };

943+ }

942

944

943\end{SaveVerbatim}

945\end{SaveVerbatim}

944\useverb{listlookup}

946\useverb{listlookup}

tutorial/views.tex+12−12

@@ -9,9 +9,9 @@ determined by whether the vector was empty or not:

10\begin{SaveVerbatim}{appdep}

12−app : Vect a n -> Vect a m -> Vect a (n + m);

12+app : Vect a n -> Vect a m -> Vect a (n + m)

13−app {n=O} [] [] = [];

13+app {n=O} [] [] = []

14−app {n=S k} (x :: xs) ys = x :: app xs ys;

14+app {n=S k} (x :: xs) ys = x :: app xs ys

16\end{SaveVerbatim}

17\useverb{appdep}

@@ -34,11 +34,11 @@ a vector filter function, defined as follows:

35\begin{SaveVerbatim}{vfilterdef}

37−filter : (a -> Bool) -> Vect a n -> (p ** Vect a p);

37+filter : (a -> Bool) -> Vect a n -> (p ** Vect a p)

38−filter p [] = ( _ ** [] );

38+filter p [] = ( _ ** [] )

39filter p (x :: xs) with filter p xs {

40 | ( _ ** xs' )

41− = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' );

41+ = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' )

42}

44\end{SaveVerbatim}

@@ -60,7 +60,7 @@ plus one:

61data Parity : Nat -> Set where

62 even : Parity (n + n)

63− | odd : Parity (S (n + n));

63+ | odd : Parity (S (n + n))

65\end{SaveVerbatim}

66\useverb{parity}

@@ -72,7 +72,7 @@ it is even or odd and constructs the predicate accordingly.

73\begin{SaveVerbatim}{parityty}

75−parity : (n:Nat) -> Parity n;

75+parity : (n:Nat) -> Parity n

77\end{SaveVerbatim}

78\useverb{parityty}

@@ -84,11 +84,11 @@ to write a function which converts a natural number to a list of binary digits

85\begin{SaveVerbatim}{natToBin}

87−natToBin : Nat -> List Bool;

87+natToBin : Nat -> List Bool

88−natToBin O = Nil;

88+natToBin O = Nil

89natToBin k with parity k {

90− natToBin (j + j) | even = False :: natToBin j;

90+ natToBin (j + j) | even = False :: natToBin j

91− natToBin (S (j + j)) | odd = True :: natToBin j;

91+ natToBin (S (j + j)) | odd = True :: natToBin j

92}

94\end{SaveVerbatim}