git.iko.soy/Idris-dev
on 385dcbf help sign in
Idris-dev/test/idrisdoc009/expected
28 lines 422 B history raw
1Data type Test.Test : Type
2 Docs for datatype Test.
3
4Constructors:
5 MkTest : Test
6
7
8Module Test:
9 Docs for module Test.
11 It is a great module. Prelude thingy:
13 > "foo" ++ "bar"
14 "foobar"
16 Imported thingy:
18 > 0.0 :+ 0.2
19 0.0 :+ 0.2
21 Type error:
23 "foo" + 2
25 From this module:
27 > MkTest
28 MkTest