git.iko.soy/Idris-dev
on 2be265d help sign in
Idris-dev/test/basic013/basic013.idr
43 lines 1.1 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 $ the (List Nat) [1..5]
40 printLn $ the (List Nat) [5..1]
41 printLn $ the (List Int) [(-1)..(-5)]
42 printLn $ the (List Nat) [1,3..5]