git.iko.soy/Idris-dev
on 465cc1c help sign in
Idris-dev/test/idrisdoc009/expected
29 lines 442 B history raw
1Type checking ./Test.idr
2Data type Test : Type
3 Docs for datatype Test.
4
5Constructors:
6 MkTest : Test
7
8
9Module Test:
10 Docs for module Test.
12 It is a great module. Prelude thingy:
14 > "foo" ++ "bar"
15 "foobar"
17 Imported thingy:
19 > 0.0 :+ 0.2
20 0.0 :+ 0.2
22 Type error:
24 "foo" + 2
26 From this module:
28 > MkTest
29 MkTest