git.iko.soy/Idris-dev
on bd8ea0a help sign in
Idris-dev/test/basic013/basic013.idr
76 lines 2.4 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 let x = 4
24 let newstr = appMany (toNat x)
25 putStrLn newstr
26 printLn (strHead newstr)
27 printLn (length newstr)
28 printLn (strIndex newstr 4)
29 putStrLn (strCons (strIndex newstr 4) "")
30 putStrLn ("Tail: " ++ strTail newstr)
31 putStrLn ("Tail Tail: " ++ strTail (strTail newstr))
32 putStrLn ("Cons: " ++ strCons 'λ' newstr)
33 putStrLn ("Reverse: " ++ reverse newstr)
34 printLn [1..5]
35 printLn [5..1]
36 printLn [(-9), (-7)..(-1)]
37 printLn [17,15..1]
38 printLn [19,15..2]
39 printLn [-2,0..4]
40 printLn [1,0..-2]
41 printLn [3,5..3]
42 printLn [2,1..2]
43 printLn [4,1..3]
44 printLn [1,4..2]
45 printLn [3,5..1]
46 printLn [4,1..5]
47 printLn [1,1..2]
48 printLn [2,2..1]
49 printLn $ the (List Nat) [1..5]
50 printLn $ the (List Nat) [5..1]
51 printLn $ the (List Nat) [5,4..1]
52 printLn $ the (List Nat) [1,3..5]
53 printLn $ the (List Nat) [5,3..1]
54 printLn $ the (List Nat) [3,5..3]
55 printLn $ the (List Nat) [2,1..2]
56 printLn $ the (List Nat) [4,1..3]
57 printLn $ the (List Nat) [1,4..2]
58 printLn $ the (List Nat) [3,5..1]
59 printLn $ the (List Nat) [4,1..5]
60 printLn $ the (List Nat) [1,1..2]
61 printLn $ the (List Nat) [2,2..1]
62 printLn $ the (List Int) [(-1)..(-5)]
63 printLn $ the (List Int) [-2,0..4]
64 printLn $ the (List Int) [1,0..-2]
65 printLn $ the (List Int) [3,5..3]
66 printLn $ the (List Int) [2,1..2]
67 printLn $ the (List Int) [4,1..3]
68 printLn $ the (List Int) [1,4..2]
69 printLn $ the (List Int) [3,5..1]
70 printLn $ the (List Int) [4,1..5]
71 printLn $ the (List Int) [1,1..2]
72 printLn $ the (List Int) [2,2..1]
73 printLn ['z'..'x']
74 printLn ['g','e'..'a']
75 printLn ['x'..'z']
76 printLn ['a','c'..'g']