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