git.iko.soy/Idris-dev
on master help sign in
Fix Curses whitespace issue with test delab001
8ff9748David Raymond Christiansen
test/delab001/expected+3−4
compare with master
unifiedsplit
@@ -1,14 +1,13 @@
1Type checking ./delab001.idr
1Type checking ./delab001.idr
2−*delab001> [?1049h(B[?7h[?1049l [?1l>foo : Nat -> String
2+foo : Nat -> String
3foo n = case n of
3foo n = case n of
4 0 => "z"
4 0 => "z"
5 S _ => "s"
5 S _ => "s"
6−*delab001> [?1049h(B[?7h[?1049l [?1l>bar : Nat -> String -> String
6+bar : Nat -> String -> String
7bar x y = case x of
7bar x y = case x of
8 0 => y
8 0 => y
9 S _ => (y ++ y)
9 S _ => (y ++ y)
10−*delab001> [?1049h(B[?7h[?1049l [?1l>append : List a -> List a -> List a
10+append : List a -> List a -> List a
11append xs ys = case xs of
11append xs ys = case xs of
12 [] => ys
12 [] => ys
13 (x :: xs) => (x :: (append xs ys))
13 (x :: xs) => (x :: (append xs ys))
14−*delab001> Bye bye
test/delab001/input+1
@@ -1,3 +1,4 @@
1+:consolewidth infinite
1:printdef foo
2:printdef foo
2:printdef bar
3:printdef bar
3:printdef append
4:printdef append