git.iko.soy/Idris-dev
on 2d0cc49 help sign in
Idris-dev/test/interactive005/input
26 lines 374 B history raw
1:consolewidth 80
2the Nat (1 + 2)
3:exec
4:c bytecode hello.bytecode
5:c c hello
6:doc main
7:reload
8:consolewidth 80
9:load interactive005.idr
10:total main
11:exec
12:consolewidth 80
13:t id
14:set showimplicits
15:t id
16:unset showimplicits
17:t id
18:warranty
19:consolewidth 10
20:doc main
21:consolewidth infinite
22:doc main
23:let data Nat2 = Zero | Succ Nat2
24:t Nat2
25:compile Test.idr
26:compile a.out