git.iko.soy/Idris-dev
on master help sign in
Idris-dev/test/basic013/basic013.idr
78 lines 2.5 kB history raw
1foo : String
2foo = "λx→x"
4bar : String
5bar = "λx→x"
7baz : Char
8baz = 'λ'
10quux : String
11quux = "\x0a\x80\xC9\xFF\n3\n4"
13appMany : Nat -> String
14appMany Z = foo
15appMany (S k) = bar ++ appMany k
17main : IO ()
18main = do putStrLn foo
19 putStrLn (foo ++ bar)
20 putStrLn (reverse (foo ++ bar))
21 printLn (length foo)
22 printLn baz
23 printLn (strCons '\x141' "")
24 printLn (singleton (chr 0x141))
25 let x = 4
26 let newstr = appMany (toNat x)
27 putStrLn newstr
28 printLn (strHead newstr)
29 printLn (length newstr)
30 printLn (strIndex newstr 4)
31 putStrLn (strCons (strIndex newstr 4) "")
32 putStrLn ("Tail: " ++ strTail newstr)
33 putStrLn ("Tail Tail: " ++ strTail (strTail newstr))
34 putStrLn ("Cons: " ++ strCons 'λ' newstr)
35 putStrLn ("Reverse: " ++ reverse newstr)
36 printLn [1..5]
37 printLn [5..1]
38 printLn [(-9), (-7)..(-1)]
39 printLn [17,15..1]
40 printLn [19,15..2]
41 printLn [-2,0..4]
42 printLn [1,0..-2]
43 printLn [3,5..3]
44 printLn [2,1..2]
45 printLn [4,1..3]
46 printLn [1,4..2]
47 printLn [3,5..1]
48 printLn [4,1..5]
49 printLn [1,1..2]
50 printLn [2,2..1]
51 printLn $ the (List Nat) [1..5]
52 printLn $ the (List Nat) [5..1]
53 printLn $ the (List Nat) [5,4..1]
54 printLn $ the (List Nat) [1,3..5]
55 printLn $ the (List Nat) [5,3..1]
56 printLn $ the (List Nat) [3,5..3]
57 printLn $ the (List Nat) [2,1..2]
58 printLn $ the (List Nat) [4,1..3]
59 printLn $ the (List Nat) [1,4..2]
60 printLn $ the (List Nat) [3,5..1]
61 printLn $ the (List Nat) [4,1..5]
62 printLn $ the (List Nat) [1,1..2]
63 printLn $ the (List Nat) [2,2..1]
64 printLn $ the (List Int) [(-1)..(-5)]
65 printLn $ the (List Int) [-2,0..4]
66 printLn $ the (List Int) [1,0..-2]
67 printLn $ the (List Int) [3,5..3]
68 printLn $ the (List Int) [2,1..2]
69 printLn $ the (List Int) [4,1..3]
70 printLn $ the (List Int) [1,4..2]
71 printLn $ the (List Int) [3,5..1]
72 printLn $ the (List Int) [4,1..5]
73 printLn $ the (List Int) [1,1..2]
74 printLn $ the (List Int) [2,2..1]
75 printLn ['z'..'x']
76 printLn ['g','e'..'a']
77 printLn ['x'..'z']
78 printLn ['a','c'..'g']