git.iko.soy/Idris-dev
on 751fb32 help sign in
Idris-dev/test/basic013/basic013.idr
34 lines 829 B 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)