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

git.iko.soy/Idris-dev

Remove semicolons in tutorial

commit2e9fcd400d0f472a70375ae4f1f6ad6310ca7013 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateFri 6 Jan 2012, 23:20 (15 years ago) parentead54e4

27 files changed+501−493

compare with master

unifiedsplit

lib/io.idr+22−22 src/Idris/Prover.hs+1−1 tutorial/classes.tex+46−46 tutorial/examples/Makefile+7 tutorial/examples/binary.idr+27−27 tutorial/examples/bmain.idr+6−6 tutorial/examples/btree.idr+11−11 tutorial/examples/classes.idr+9−9 tutorial/examples/foo.idr+5−5 tutorial/examples/hello.idr+3−3 tutorial/examples/interp.idr+36−36 tutorial/examples/letbind.idr+8−8 tutorial/examples/prims.idr+9−9 tutorial/examples/theorems.idr+17−17 tutorial/examples/usefultypes.idr+12−12 tutorial/examples/vbroken.idr+3−4 tutorial/examples/views.idr+14−14 tutorial/idris-tutorial.pdf tutorial/interp.tex+38−38 tutorial/intro.tex+1−1 tutorial/miscellany.tex+16−16 tutorial/modules.tex+33−33 tutorial/provisional.tex+32−32 tutorial/starting.tex+3−3 tutorial/theorems.tex+19−19 tutorial/typesfuns.tex+111−109 tutorial/views.tex+12−12

lib/io.idr+22−22

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

1−import prelude.list;

1+import prelude.list

33%access public

5−abstract data IO a = prim__IO a;

5+abstract data IO a = prim__IO a

77abstract

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

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

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

9+io_bind (prim__IO v) k = k v

1010

1111abstract

12−io_return : a -> IO a;

13−io_return x = prim__IO x;

12+io_return : a -> IO a

13+io_return x = prim__IO x

1414

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

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

1717

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

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

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

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

2020

2222

23−interpFTy : FTy -> Set;

24−interpFTy FInt = Int;

25−interpFTy FFloat = Float;

26−interpFTy FChar = Char;

27−interpFTy FString = String;

28−interpFTy FPtr = Ptr;

29−interpFTy FUnit = ();

23+interpFTy : FTy -> Set

24+interpFTy FInt = Int

25+interpFTy FFloat = Float

26+interpFTy FChar = Char

27+interpFTy FString = String

28+interpFTy FPtr = Ptr

29+interpFTy FUnit = ()

3030

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

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

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

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

34− mkForeign' Nil ty = ty;

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

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

34+ mkForeign' Nil ty = ty

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

3636}

3737

3838

3939data Foreign : Set -> Set where

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

41− Foreign (ForeignTy xs t);

41+ Foreign (ForeignTy xs t)

4242

43−mkForeign : Foreign x -> x;

43+mkForeign : Foreign x -> x

4444-- mkForeign compiled as primitive

4545

4646

src/Idris/Prover.hs+1−1

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

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

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

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

31− "\n};\n"

31+ "\n}\n"

3232

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

3434prove ctxt n ty

tutorial/classes.tex+46−46

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

1717\begin{SaveVerbatim}{showclass}

1818

1919class Show a where {

20− show : a -> String;

20+ show : a -> String

2121}

2222

2323\end{SaveVerbatim}

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

2929

3030\begin{SaveVerbatim}{showty}

3131

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

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

3333

3434\end{SaveVerbatim}

3535\useverb{showty}

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

4444\begin{SaveVerbatim}{shownat}

4545

4646instance Show Nat where {

47− show O = "O";

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

47+ show O = "O"

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

4949}

5050

5151Idris> show (S (S (S O)))

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

6464

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

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

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

68− show' VNil = "";

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

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

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

68+ show' VNil = ""

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

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

7171 }

7272}

7373

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

8282\begin{SaveVerbatim}{eqbasic}

8383

8484class Eq a where {

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

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

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

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

8787}

8888

8989\end{SaveVerbatim}

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

9696\begin{SaveVerbatim}{eqnat}

9797

9898instance Eq Nat where {

99− O == O = True;

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

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

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

99+ O == O = True

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

101+ O == (S y) = False

102+ (S x) == O = False

103103

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

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

105105}

106106

107107\end{SaveVerbatim}

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

116116\begin{SaveVerbatim}{eqdefault}

117117

118118class Eq a where {

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

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

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

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

121121

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

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

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

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

124124}

125125

126126\end{SaveVerbatim}

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

139139

140140\begin{SaveVerbatim}{ord}

141141

142−data Ordering = LT | EQ | GT;

142+data Ordering = LT | EQ | GT

143143

144144\end{SaveVerbatim}

145145\useverb{ord}

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

147147\begin{SaveVerbatim}{eqord}

148148

149149class Eq a => Ord a where {

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

151−

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

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

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

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

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

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

150+ compare : a -> a -> Ordering

151+

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

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

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

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

156+ max : a -> a -> a

157+ min : a -> a -> a

158158}

159159

160160\end{SaveVerbatim}

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

171171

172172\begin{SaveVerbatim}{sortty}

173173

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

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

175175

176176\end{SaveVerbatim}

177177\useverb{sortty}

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

182182

183183\begin{SaveVerbatim}{sortshow}

184184

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

186−sortAndShow xs = show (sort xs);

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

186+sortAndShow xs = show (sort xs)

187187

188188\end{SaveVerbatim}

189189\useverb{sortshow}

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

201201\begin{SaveVerbatim}{monad}

202202

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

204− return : a -> m a;

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

204+ return : a -> m a

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

206206}

207207

208208\end{SaveVerbatim}

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

226226\begin{SaveVerbatim}{maybemonad}

227227

228228instance Monad Maybe where {

229− return = Just;

229+ return = Just

230230

231− Nothing >>= k = Nothing;

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

231+ Nothing >>= k = Nothing

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

233233}

234234

235235\end{SaveVerbatim}

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

241241

242242\begin{SaveVerbatim}{maybeadd}

243243

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

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

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

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

248− };

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

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

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

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

248+ }

249249

250250\end{SaveVerbatim}

251251\useverb{maybeadd}

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

274274\begin{SaveVerbatim}{monadplus}

275275

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

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

278− mzero : m a;

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

278+ mzero : m a

279279}

280280

281281\end{SaveVerbatim}

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

299299

300300\begin{SaveVerbatim}{guardq}

301301

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

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

303303

304304\end{SaveVerbatim}

305305\useverb{guardq}

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

319319

320320\begin{SaveVerbatim}{maddb}

321321

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

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

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

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

324324\end{SaveVerbatim}

325325\useverb{maddb}

326326

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

33data Binary : Nat -> Set where

44 bEnd : Binary O

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

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

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

88instance Show (Binary n) where {

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

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

11− show bEnd = "";

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

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

11+ show bEnd = ""

1212}

1313

1414data Parity : Nat -> Set where

1515 even : Parity (n + n)

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

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

1717

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

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

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

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

19+parity O = even {n=O}

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

2121parity (S (S k)) with parity k {

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

23− parity (S (S (S (j + j)))) | odd ?= odd {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}

2424}

2525

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

27−natToBin O = bEnd;

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

27+natToBin O = bEnd

2828natToBin (S k) with parity k {

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

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

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

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

3131}

3232

33−intToNat : Int -> Nat;

34−intToNat 0 = O;

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

33+intToNat : Int -> Nat

34+intToNat 0 = O

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

3636

37−main : IO ();

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

39− x <- getLine;

40− let n = prim__strToInt x;

41− let b = natToBin (fromInteger n);

42− print b; };

37+main : IO ()

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

39+ x <- getLine

40+ let n = prim__strToInt x

41+ let b = natToBin (fromInteger n)

42+ print b }

4343

4444---------- Proofs ----------

4545

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

4848 intro;

4949 rewrite plusn_Sm j j;

5050 trivial;

51−};

51+}

5252

5353parity_lemma_2 = proof {

5454 intro;

5555 intro;

5656 rewrite plusn_Sm j j;

5757 trivial;

58−};

58+}

5959

6060parity_lemma_1 = proof {

6161 intro j;

6262 intro;

6363 rewrite plusn_Sm j j;

6464 trivial;

65−};

65+}

6666

6767

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 ();

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

7− print (toList t);

8− };

5+main : IO ()

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

7+ print (toList t)

8+ }

tutorial/examples/btree.idr+11−11

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

1−module btree;

1+module btree

33data 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;

7−insert x Leaf = Node Leaf x Leaf;

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

7+insert x Leaf = Node Leaf x Leaf

88insert 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))

1010

11−toList : BTree a -> List a;

12−toList Leaf = [];

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

11+toList : BTree a -> List a

12+toList Leaf = []

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

1414

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

16−toTree [] = Leaf;

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

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

16+toTree [] = Leaf

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

1818

tutorial/examples/classes.idr+9−9

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

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

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

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

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

5− };

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

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

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

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

5+ }

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

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

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

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

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

11−sortAndShow xs = show (sort xs);

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

11+sortAndShow xs = show (sort xs)

tutorial/examples/foo.idr+5−5

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

1−module foo;

1+module foo

33namespace x {

4− test : Int -> Int;

5− test x = x * 2;

4+ test : Int -> Int

5+ test x = x * 2

66}

88namespace y {

9− test : String -> String;

10− test x = x ++ x;

9+ test : String -> String

10+ test x = x ++ x

1111}

1212

tutorial/examples/hello.idr+3−3

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

1−module main;

1+module main

3−main : IO ();

4−main = putStrLn "Hello world";

3+main : IO ()

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;

6−interpTy TyInt = Int;

7−interpTy TyBool = Bool;

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

5+interpTy : Ty -> Set

6+interpTy TyInt = Int

7+interpTy TyBool = Bool

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

1010using (G : Vect Ty n) {

1111

1212 data Env : Vect Ty n -> Set where

1313 Nil : Env Nil

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

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

1515

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

1717 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

1919

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

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

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

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

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

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

2323

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

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

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

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

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

3030 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

3232

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

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

35− interp env (Val x) = x;

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

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

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

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

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

35+ interp env (Val x) = x

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

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)

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

4040

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

42− eId = Lam (Var stop);

41+ eId : Expr G (TyFun TyInt TyInt)

42+ eId = Lam (Var stop)

4343

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

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

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

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

4646

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

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

47+ eDouble : Expr G (TyFun TyInt TyInt)

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

4949

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

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

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

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

5252

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

53+ fact : Expr G (TyFun TyInt TyInt)

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

5656

5757}

5858

59−testFac : Int;

60−testFac = interp [] fact 4;

59+testFac : Int

60+testFac = interp [] fact 4

6161

62−main : IO ();

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

64− x <- getLine;

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

66− };

62+main : IO ()

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

64+ x <- getLine

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

66+ }

6767

6868

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

44mirror 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

1010showPerson p = let MkPerson name age = p in

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

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

1212

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

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

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

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

16− };

16+ }

1717

tutorial/examples/prims.idr+9−9

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

1−module prims;

1+module prims

3−x : Int;

4−x = 42;

3+x : Int

4+x = 42

6−foo : String;

7−foo = "Sausage machine";

6+foo : String

7+foo = "Sausage machine"

9−bar : Char;

10−bar = 'Z';

9+bar : Char

10+bar = 'Z'

1111

12−quux : Bool;

13−quux = False;

12+quux : Bool

13+quux = False

1414

tutorial/examples/theorems.idr+17−17

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

2−fiveIsFive : 5 = 5;

3−fiveIsFive = refl;

2+fiveIsFive : 5 = 5

3+fiveIsFive = refl

5−twoPlusTwo : 2 + 2 = 4;

6−twoPlusTwo = refl;

5+twoPlusTwo : 2 + 2 = 4

6+twoPlusTwo = refl

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

9−plusReduces n = refl;

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

9+plusReduces n = refl

1010

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

12−plusReducesO O = refl;

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

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

12+plusReducesO O = refl

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

1414

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

16−plusReducesS O m = refl;

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

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

16+plusReducesS O m = refl

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

1818

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

20−plusReducesO' O = ?plusredO_O;

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

20+plusReducesO' O = ?plusredO_O

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

22− ?plusredO_S;

22+ ?plusredO_S

2323

2424

2525---------- Proofs ----------

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

2929 intro;

3030 rewrite ih;

3131 trivial;

32−};

32+}

3333

3434plusredO_O = proof {

3535 compute;

3636 trivial;

37−};

37+}

3838

tutorial/examples/usefultypes.idr+12−12

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

2−intVec : Vect Int 5;

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

2+intVec : Vect Int 5

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

5−double : Int -> Int;

6−double x = x * 2;

5+double : Int -> Int

6+double x = x * 2

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

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

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

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

1010

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

12−list_lookup _ Nil = Nothing;

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

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

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

12+list_lookup _ Nil = Nothing

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

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

1515

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

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

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

1818 Nothing => def

1919 | Just x => x

20− };

20+ }

2121

tutorial/examples/vbroken.idr+3−4

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

1−

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

3−vapp Nil ys = ys;

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

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

2+vapp Nil ys = ys

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

33data Parity : Nat -> Set where

44 even : Parity (n + n)

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

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

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

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

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

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

8+parity O = even {n=O}

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

1010parity (S (S k)) with parity k {

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

12− parity (S (S (S (j + j)))) | odd ?= odd {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}

1313}

1414

1515

16−natToBin : Nat -> List Bool;

17−natToBin O = Nil;

16+natToBin : Nat -> List Bool

17+natToBin O = Nil

1818natToBin k with parity k {

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

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

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

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

2121}

2222

2323

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

2828 intro;

2929 rewrite plusn_Sm j j;

3030 trivial;

31−};

31+}

3232

3333views.parity_lemma_1 = proof {

34− intro j;

34+ intro;

3535 intro;

3636 rewrite plusn_Sm j j;

3737 trivial;

38−};

38+}

3939

4040

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}:

1010\begin{SaveVerbatim}{tydecl}

1111

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

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

1313

1414\end{SaveVerbatim}

1515\useverb{tydecl}

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

2020

2121\begin{SaveVerbatim}{interpty}

2222

23−interpTy : Ty -> Set;

24−interpTy TyInt = Int;

25−interpTy TyBool = Bool;

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

23+interpTy : Ty -> Set

24+interpTy TyInt = Int

25+interpTy TyBool = Bool

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

2727

2828\end{SaveVerbatim}

2929\useverb{interpty}

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

6262

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

6464 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

6666

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

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

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

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

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

7373 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

7575

7676\end{SaveVerbatim}

7777\codefig{exprty}{Expression representation}

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

8686

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

8888 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

9090

9191\end{SaveVerbatim}

9292\useverb{hastype}

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

163163

164164\begin{SaveVerbatim}{ifcon}

165165

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

167167

168168\end{SaveVerbatim}

169169\useverb{ifcon}

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

180180

181181data Env : Vect Ty n -> Set where

182182 Nil : Env Nil

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

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

184184

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

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

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

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

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

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

188188

189189\end{SaveVerbatim}

190190\useverb{envtype}

191191

192192\begin{SaveVerbatim}{interpdef}

193193

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

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

196−interp env (Val x) = x;

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

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

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

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

196+interp env (Val x) = x

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

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)

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

201− else (interp env e);

201+ else (interp env e)

202202

203203\end{SaveVerbatim}

204204\codefig{interpdef}{Intepreter definition}

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

210210

211211\begin{SaveVerbatim}{interpty}

212212

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

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

214214

215215\end{SaveVerbatim}

216216\useverb{interpty}

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

220220

221221\begin{SaveVerbatim}{varinterp}

222222

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

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

224224

225225\end{SaveVerbatim}

226226\useverb{varinterp}

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

230230

231231\begin{SaveVerbatim}{valinterp}

232232

233−interp env (Val x) = x;

233+interp env (Val x) = x

234234

235235\end{SaveVerbatim}

236236\useverb{valinterp}

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

242242

243243\begin{SaveVerbatim}{laminterp}

244244

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

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

246246

247247\end{SaveVerbatim}

248248\useverb{laminterp}

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

254254

255255\begin{SaveVerbatim}{appinterp}

256256

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

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

258258

259259\end{SaveVerbatim}

260260\useverb{appinterp}

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

267267

268268\begin{SaveVerbatim}{opinterp}

269269

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)

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

272− else (interp env e);

272+ else (interp env e)

273273

274274\end{SaveVerbatim}

275275\useverb{opinterp}

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

280280

281281\begin{SaveVerbatim}{addtest}

282282

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

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

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

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

285285

286286\end{SaveVerbatim}

287287\useverb{addtest}

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

293293

294294\begin{SaveVerbatim}{lazyapp}

295295

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

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

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

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

298298

299299\end{SaveVerbatim}

300300\useverb{lazyapp}

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

306306

307307\begin{SaveVerbatim}{facttest}

308308

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

309+fact : Expr G (TyFun TyInt TyInt)

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

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

312− (Var stop)));

312+ (Var stop)))

313313

314314\end{SaveVerbatim}

315315\useverb{facttest}

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

319319

320320\begin{SaveVerbatim}{factmain}

321321

322−main : IO ();

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

324− x <- getLine;

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

326− };

322+main : IO ()

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

324+ x <- getLine

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

326+ }

327327

328328\end{SaveVerbatim}

329329\useverb{factmain}

tutorial/intro.tex+1−1

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

3333

3434\begin{SaveVerbatim}{appendv}

3535

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

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

3737

3838\end{SaveVerbatim}

3939\useverb{appendv}

tutorial/miscellany.tex+16−16

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

1515

1616\begin{SaveVerbatim}{litidr}

1717

18−> module literate;

18+> module literate

1919

2020This is a comment. The main program is below

2121

22−> main : IO ();

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

22+> main : IO ()

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

2424

2525\end{SaveVerbatim}

2626\useverb{litidr}

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

4141

4242\begin{SaveVerbatim}{foreignty}

4343

4545

4646\end{SaveVerbatim}

4747\useverb{foreignty}

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

5454

5555\begin{SaveVerbatim}{interpfty}

5656

57−interpFTy : FTy -> Set;

58−interpFTy FInt = Int;

59−interpFTy FFloat = Float;

60−interpFTy FChar = Char;

61−interpFTy FString = String;

62−interpFTy FPtr = Ptr;

63−interpFTy FUnit = ();

57+interpFTy : FTy -> Set

58+interpFTy FInt = Int

59+interpFTy FFloat = Float

60+interpFTy FChar = Char

61+interpFTy FString = String

62+interpFTy FPtr = Ptr

63+interpFTy FUnit = ()

6464

6565\end{SaveVerbatim}

6666\useverb{interpfty}

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

7171

7272\begin{SaveVerbatim}{ffunty}

7373

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

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

7575

7676\end{SaveVerbatim}

7777\useverb{ffunty}

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

100100

101101data Foreign : Set -> Set where

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

103− Foreign (ForeignTy xs t);

103+ Foreign (ForeignTy xs t)

104104

105−mkForeign : Foreign x -> x;

105+mkForeign : Foreign x -> x

106106

107107\end{SaveVerbatim}

108108\useverb{mkForeign}

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

113113

114114\begin{SaveVerbatim}{putStrex}

115115

116−putStr : String -> IO ();

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

116+putStr : String -> IO ()

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

118118\end{SaveVerbatim}

119119\useverb{putStrex}

120120

tutorial/modules.tex+33−33

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

1212

1313\begin{SaveVerbatim}{bstmod}

1414

15−module btree;

15+module btree

1616

1717data BTree a = Leaf

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

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

1919

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

21−insert x Leaf = Node Leaf x Leaf;

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

21+insert x Leaf = Node Leaf x Leaf

2222insert 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))

2424

25−toList : BTree a -> List a;

26−toList Leaf = [];

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

25+toList : BTree a -> List a

26+toList Leaf = []

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

2828

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

30−toTree [] = Leaf;

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

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

30+toTree [] = Leaf

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

3232

3333\end{SaveVerbatim}

3434\codefig{bstmod}{Binary Tree module}

3535

3636\begin{SaveVerbatim}{bstmain}

3737

38−module main;

38+module main

3939

40−import btree;

40+import btree

4141

42−main : IO ();

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

44− print (toList t);

45− };

42+main : IO ()

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

44+ print (toList t)

45+ }

4646

4747\end{SaveVerbatim}

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

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

9797

9898\begin{SaveVerbatim}{bstmodp}

9999

100−module btree;

100+module btree

101101

102102abstract data BTree a = Leaf

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

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

104104

105105abstract

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

107−insert x Leaf = Node Leaf x Leaf;

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

107+insert x Leaf = Node Leaf x Leaf

108108insert 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))

110110

111111abstract

112−toList : BTree a -> List a;

113−toList Leaf = [];

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

112+toList : BTree a -> List a

113+toList Leaf = []

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

115115

116116abstract

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

118−toTree [] = Leaf;

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

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

118+toTree [] = Leaf

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

120120

121121\end{SaveVerbatim}

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

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

144144

145145\begin{SaveVerbatim}{nsfoo}

146146

147−module foo;

147+module foo

148148

149149namespace x {

150− test : Int -> Int;

151− test x = x * 2;

150+ test : Int -> Int

151+ test x = x * 2

152152}

153153

154154namespace y {

155− test : String -> String;

156− test x = x ++ x;

155+ test : String -> String

156+ test x = x ++ x

157157}

158158

159159\end{SaveVerbatim}

tutorial/provisional.tex+32−32

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

1010data Parity : Nat -> Set where

1111 even : Parity (n + n)

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

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

1313

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

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

1515

1616\end{SaveVerbatim}

1717\useverb{pardecl}

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

2121

2222\begin{SaveVerbatim}{parfail}

2323

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

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

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

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

25+parity O = even {n=O}

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

2727parity (S (S k)) with parity k {

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

29− parity (S (S (S (j + j)))) | odd = odd {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}

3030}

3131

3232\end{SaveVerbatim}

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

7777

7878\begin{SaveVerbatim}{paritypro}

7979

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

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

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

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

81+parity O = even {n=O}

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

8383parity (S (S k)) with parity k {

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

85− parity (S (S (S (j + j)))) | odd ?= odd {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}

8686}

8787

8888\end{SaveVerbatim}

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

128128

129129\begin{SaveVerbatim}{plusnsm}

130130

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)

132132

133133\end{SaveVerbatim}

134134\useverb{plusnsm}

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

182182

183183\begin{SaveVerbatim}{believe}

184184

185−believe_me : a -> b;

185+believe_me : a -> b

186186

187187\end{SaveVerbatim}

188188\useverb{believe}

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

198198 intro;

199199 intro;

200200 exact believe_me value;

201−};

201+}

202202

203203\end{SaveVerbatim}

204204\useverb{pladodgy}

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

221221data Binary : Nat -> Set where

222222 bEnd : Binary O

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

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

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

225225

226226\end{SaveVerbatim}

227227\useverb{bindef}

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

238238

239239\begin{SaveVerbatim}{ntbty}

240240

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

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

242242

243243\end{SaveVerbatim}

244244\useverb{ntbty}

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

250250

251251\begin{SaveVerbatim}{ntbdef}

252252

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

254−natToBin O = bEnd;

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

254+natToBin O = bEnd

255255natToBin (S k) with parity k {

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

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

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

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

258258}

259259

260260\end{SaveVerbatim}

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

271271 intro;

272272 rewrite plusn_Sm j j;

273273 trivial;

274−};

274+}

275275

276276\end{SaveVerbatim}

277277\useverb{ntboddprf}

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

282282

283283\begin{SaveVerbatim}{binmain}

284284

285−main : IO ();

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

287− x <- getLine;

288− let n = prim__strToInt x;

289− let b = natToBin (fromInteger n);

290− print b;

291− };

285+main : IO ()

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

287+ x <- getLine

288+ let n = prim__strToInt x

289+ let b = natToBin (fromInteger n)

290+ print b

291+ }

292292

293293\end{SaveVerbatim}

294294\useverb{binmain}

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

299299\begin{SaveVerbatim}{showbin}

300300

301301instance Show (Binary n) where {

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

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

304− show bEnd = "";

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

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

304+ show bEnd = ""

305305}

306306

307307\end{SaveVerbatim}

tutorial/starting.tex+3−3

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

4141

4242\begin{SaveVerbatim}{hello}

4343

44−module main;

44+module main

4545

46−main : IO();

47−main = putStrLn "Hello world";

46+main : IO ()

47+main = putStrLn "Hello world"

4848

4949\end{SaveVerbatim}

5050\useverb{hello}

tutorial/theorems.tex+19−19

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

99\begin{SaveVerbatim}{}

1010

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

12− refl : x = x;

12+ refl : x = x

1313

1414\end{SaveVerbatim}

1515\useverb{}

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

2020

2121\begin{SaveVerbatim}{eqprf}

2222

23−fiveIsFive : 5 = 5;

24−fiveIsFive = refl;

23+fiveIsFive : 5 = 5

24+fiveIsFive = refl

2525

26−twoPlusTwo : 2 + 2 = 4;

27−twoPlusTwo = refl;

26+twoPlusTwo : 2 + 2 = 4

27+twoPlusTwo = refl

2828

2929\end{SaveVerbatim}

3030\useverb{eqprf}

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

3636

3737\begin{SaveVerbatim}{plusred}

3838

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

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

4040

4141\end{SaveVerbatim}

4242\useverb{plusred}

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

5555

5656\begin{SaveVerbatim}{plusredp}

5757

58−plusReduces n = refl;

58+plusReduces n = refl

5959

6060\end{SaveVerbatim}

6161\useverb{plusredp}

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

6767

6868\begin{SaveVerbatim}{plusRedO}

6969

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

71−plusReducesO O = refl;

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

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

71+plusReducesO O = refl

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

7373

7474\end{SaveVerbatim}

7575\useverb{plusRedO}

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

8080

8181\begin{SaveVerbatim}{resps}

8282

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

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

8484

8585\end{SaveVerbatim}

8686\useverb{resps}

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

9090

9191\begin{SaveVerbatim}{plusRedS}

9292

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

94−plusReducesS O m = refl;

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

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

94+plusReducesS O m = refl

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

9696

9797\end{SaveVerbatim}

9898\useverb{plusRedS}

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

114114

115115\begin{SaveVerbatim}{prOstruct}

116116

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

118−plusReducesO' O = ?plusredO_O;

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

118+plusReducesO' O = ?plusredO_O

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

120− ?plusredO_S;

120+ ?plusredO_S

121121

122122\end{SaveVerbatim}

123123\useverb{prOstruct}

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

208208plusredO_O = proof {

209209 compute;

210210 refine refl;

211−};

211+}

212212

213213\end{SaveVerbatim}

214214\useverb{prOprooftrace}

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

286286 intro;

287287 rewrite ih;

288288 trivial;

289−};

289+}

290290

291291\end{SaveVerbatim}

292292\useverb{prOStrace}

tutorial/typesfuns.tex+111−109

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

1313

1414\begin{SaveVerbatim}{constprims}

1515

16−module prims;

16+module prims

1717

18−x : Int;

19−x = 42;

18+x : Int

19+x = 42

2020

21−foo : String;

22−foo = "Sausage machine";

21+foo : String

22+foo = "Sausage machine"

2323

24−bar : Char;

25−bar = 'Z';

24+bar : Char

25+bar = 'Z'

2626

27−quux : Bool;

28−quux = False;

27+quux : Bool

28+quux = False

2929

3030\end{SaveVerbatim}

3131\useverb{constprims}

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

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

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

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

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

39−component is separated by a semi-colon.

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

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.

4042

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

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

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

7678

7779\begin{SaveVerbatim}{natlist}

7880

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

80− -- (zero and successor)

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

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

82+ -- (zero and successor)

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

8284

8385\end{SaveVerbatim}

8486\useverb{natlist}

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

9395

9496\begin{SaveVerbatim}{infixcons}

9597

96−infixr 7 :: ;

98+infixr 7 ::

9799

98100\end{SaveVerbatim}

99101\useverb{infixcons}

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

124126\begin{SaveVerbatim}{natfns}

125127

126128-- Unary addition

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

128−plus O y = y;

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

129+plus : Nat -> Nat -> Nat

130+plus O y = y

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

130132

131133-- Unary multiplication

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

133−mult O y = O;

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

134+mult : Nat -> Nat -> Nat

135+mult O y = O

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

135137

136138\end{SaveVerbatim}

137139\useverb{natfns}

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

186188

187189\begin{SaveVerbatim}{revwhere}

188190

189−rev : List a -> List a;

191+rev : List a -> List a

190192rev xs = revAcc [] xs where {

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

192− revAcc acc [] = acc;

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

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

194+ revAcc acc [] = acc

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

194196}

195197

196198\end{SaveVerbatim}

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

207209

208210\begin{SaveVerbatim}{revwhereb}

209211

210−rev : List a -> List a;

212+rev : List a -> List a

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

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

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

213215 ...

214216}

215217

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

228230

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

230232 Nil : Vect a O

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

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

232234

233235\end{SaveVerbatim}

234236\useverb{vect}

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

257259

258260\begin{SaveVerbatim}{vapp}

259261

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

261−app Nil ys = ys;

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

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

263+app Nil ys = ys

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

263265

264266\end{SaveVerbatim}

265267\useverb{vapp}

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

270272

271273\begin{SaveVerbatim}{vapperr}

272274

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

274−app Nil ys = ys;

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

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

276+app Nil ys = ys

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

276278

277279\end{SaveVerbatim}

278280\useverb{vapperr}

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

303305

304306data Fin : Nat -> Set where

305307 fO : Fin (S k)

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

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

307309

308310\end{SaveVerbatim}

309311\useverb{findecl}

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

321323

322324\begin{SaveVerbatim}{vlookup}

323325

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

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

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

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

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

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

327329

328330\end{SaveVerbatim}

329331\useverb{vlookup}

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

384386

385387\begin{SaveVerbatim}{vlookupn}

386388

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

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

388390

389391\end{SaveVerbatim}

390392\useverb{vlookupn}

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

406408

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

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

410412

411413\end{SaveVerbatim}

412414\useverb{elem}

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

419421

420422\begin{SaveVerbatim}{testelem}

421423

422−testVec : Vect Int 4;

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

424+testVec : Vect Int 4

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

424426

425−inVect : Elem 5 testVec;

426−inVect = there (there here);

427+inVect : Elem 5 testVec

428+inVect = there (there here)

427429

428430\end{SaveVerbatim}

429431\useverb{testelem}

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

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

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

440442 here : Elem x (x :: xs)

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

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

442444}

443445

444446\end{SaveVerbatim}

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

454456

455457\begin{SaveVerbatim}{ioty}

456458

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

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

458460

459461\end{SaveVerbatim}

460462\useverb{ioty}

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

467469

468470\begin{SaveVerbatim}{main}

469471

470−main : IO ();

471−main = putStrLn "Hello world";

472+main : IO ()

473+main = putStrLn "Hello world"

472474

473475\end{SaveVerbatim}

474476\useverb{main}

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

479481

480482\begin{SaveVerbatim}{putstr}

481483

482−putStrLn : String -> IO ();

483−putStr : String -> IO ();

484+putStrLn : String -> IO ()

485+putStr : String -> IO ()

484486

485487\end{SaveVerbatim}

486488

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

488490

489491\begin{SaveVerbatim}{getline}

490492

491−getLine : IO String;

493+getLine : IO String

492494

493495\end{SaveVerbatim}

494496\useverb{getline}

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

499501

500502\begin{SaveVerbatim}{fileops}

501503

502−data File; -- abstract

503−data Mode = Read | Write | ReadWrite;

504+data File -- abstract

505+data Mode = Read | Write | ReadWrite

504506

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

506−closeFile : File -> IO ();

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

508+closeFile : File -> IO ()

507509

508−fread : File -> IO String;

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

510−feof : File -> IO Bool;

510+fread : File -> IO String

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

512+feof : File -> IO Bool

511513

512−readFile : String -> IO String;

514+readFile : String -> IO String

513515

514516\end{SaveVerbatim}

515517\useverb{fileops}

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

525527

526528\begin{SaveVerbatim}{greet}

527529

528−greet : IO ();

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

530− name <- getLine;

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

532− };

530+greet : IO ()

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

532+ name <- getLine

533+ putStrLn ("Hello " ++ name)

534+ }

533535

534536\end{SaveVerbatim}

535537\useverb{greet}

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

544546

545547\begin{SaveVerbatim}{return}

546548

547−return : a -> IO a;

549+return : a -> IO a

548550

549551\end{SaveVerbatim}

550552\useverb{return}

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

566568

567569\begin{SaveVerbatim}{listvec}

568570

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

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

570572

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

572574 Nil : Vect a O

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

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

574576

575577\end{SaveVerbatim}

576578\useverb{listvec}

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

594596

595597\begin{SaveVerbatim}{map}

596598

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

598−map f [] = [];

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

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

600+map f [] = []

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

600602

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

602−map f [] = [];

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

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

604+map f [] = []

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

604606

605607\end{SaveVerbatim}

606608\useverb{map}

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

610612

611613\begin{SaveVerbatim}{dvect}

612614

613−intVec : Vect Int 5;

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

615+intVec : Vect Int 5

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

615617

616−double : Int -> Int;

617−double x = x * 2;

618+double : Int -> Int

619+double x = x * 2

618620

619621\end{SaveVerbatim}

620622\useverb{dvect}

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

679681

680682\begin{SaveVerbatim}{maybe}

681683

682−data Maybe a = Just a | Nothing;

684+data Maybe a = Just a | Nothing

683685

684686\end{SaveVerbatim}

685687\useverb{maybe}

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

691693

692694\begin{SaveVerbatim}{lookuplist}

693695

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

695−list_lookup _ Nil = Nothing;

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

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

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

697+list_lookup _ Nil = Nothing

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

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

698700

699701\end{SaveVerbatim}

700702\useverb{lookuplist}

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

705707

706708\begin{SaveVerbatim}{maybefn}

707709

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

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

709711

710712\end{SaveVerbatim}

711713\useverb{maybefn}

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

724726

725727\begin{SaveVerbatim}{mkpair}

726728

727−data Pair a b = MkPair a b;

729+data Pair a b = MkPair a b

728730

729731\end{SaveVerbatim}

730732\useverb{mkpair}

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

736738

737739\begin{SaveVerbatim}{tuple}

738740

739−fred : (String, Int);

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

741+fred : (String, Int)

742+fred = ("Fred", 42)

741743

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

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

744+jim : (String, Int, String)

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

744746

745747\end{SaveVerbatim}

746748\useverb{tuple}

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

753755\begin{SaveVerbatim}{sigma}

754756

755757data 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

757759

758760\end{SaveVerbatim}

759761\useverb{sigma}

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

766768

767769\begin{SaveVerbatim}{dvec}

768770

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

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

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

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

771773

772774\end{SaveVerbatim}

773775\useverb{dvec}

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

780782

781783\begin{SaveVerbatim}{dvec1}

782784

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

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

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

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

785787

786788\end{SaveVerbatim}

787789\useverb{dvec1}

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

792794

793795\begin{SaveVerbatim}{dvec2}

794796

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

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

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

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

797799

798800\end{SaveVerbatim}

799801\useverb{dvec2}

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

806808

807809\begin{SaveVerbatim}{vfilter}

808810

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

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

810812

811813\end{SaveVerbatim}

812814\useverb{vfilter}

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

816818

817819\begin{SaveVerbatim}{vfilternil}

818820

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

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

820822

821823\end{SaveVerbatim}

822824\useverb{vfilternil}

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

830832\begin{SaveVerbatim}{vfiltercons}

831833

832834filter 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')

834836}

835837

836838\end{SaveVerbatim}

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

847849

848850\begin{SaveVerbatim}{letb}

849851

850−mirror : List a -> List a;

852+mirror : List a -> List a

851853mirror xs = let xs' = rev xs in

852− app xs xs';

854+ app xs xs'

853855

854856\end{SaveVerbatim}

855857\useverb{letb}

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

860862

861863\begin{SaveVerbatim}{letp}

862864

863−data Person = MkPerson String Int;

865+data Person = MkPerson String Int

864866

865−showPerson : Person -> String;

867+showPerson : Person -> String

866868showPerson p = let MkPerson name age = p in

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

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

868870

869871\end{SaveVerbatim}

870872\useverb{letp}

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

891893

892894\begin{SaveVerbatim}{triples}

893895

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

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

895897pythag 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 ]

897899

898900\end{SaveVerbatim}

899901\useverb{triples}

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

913915

914916\begin{SaveVerbatim}{split}

915917

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

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

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

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

919− };

921+ }

920922

921923\end{SaveVerbatim}

922924\useverb{split}

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

934936

935937\begin{SaveVerbatim}{listlookup}

936938

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

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

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

939941 Nothing => def

940942 | Just x => x

941− };

943+ }

942944

943945\end{SaveVerbatim}

944946\useverb{listlookup}

tutorial/views.tex+12−12

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

1010\begin{SaveVerbatim}{appdep}

1111

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

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

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

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

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

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

1515

1616\end{SaveVerbatim}

1717\useverb{appdep}

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

3434

3535\begin{SaveVerbatim}{vfilterdef}

3636

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

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

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

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

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

4040 | ( _ ** xs' )

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

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

4242}

4343

4444\end{SaveVerbatim}

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

6060

6161data Parity : Nat -> Set where

6262 even : Parity (n + n)

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

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

6464

6565\end{SaveVerbatim}

6666\useverb{parity}

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

7272

7373\begin{SaveVerbatim}{parityty}

7474

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

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

7676

7777\end{SaveVerbatim}

7878\useverb{parityty}

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

8484

8585\begin{SaveVerbatim}{natToBin}

8686

87−natToBin : Nat -> List Bool;

88−natToBin O = Nil;

87+natToBin : Nat -> List Bool

88+natToBin O = Nil

8989natToBin k with parity k {

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

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

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

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

9292}

9393

9494\end{SaveVerbatim}