git.iko.soy/Idris-dev
on master help sign in
Amended the test suite to report updated documentation.
8fe28aaJan de Muijnck-Hughes
test/docs001/expected+1−1
compare with master
unifiedsplit
@@ -8,7 +8,7 @@ Methods:
8 m : C t => t
8 m : C t => t
9 member of interface
9 member of interface
10
10
11− The function is Total
11+ The function is: Total & public export
12Implementations:
12Implementations:
13 C A
13 C A
14 implementation of interface
14 implementation of interface
test/docs002/expected+3−3
@@ -1,12 +1,12 @@
1T1 : Type
1T1 : Type
2 Some documentation
2 Some documentation
3
3
4− The function is Total
4+ The function is: Total & public export
5T2 : Type
5T2 : Type
6 Some other documentation
6 Some other documentation
7
7
8− The function is Total
8+ The function is: Total & public export
9T3 : Int
9T3 : Int
10 Some provided postulate
10 Some provided postulate
11
11
12− The function is not yet checked for totality
12+ The function is: not yet checked for totality & public export
test/docs003/expected+3−1
@@ -8,7 +8,7 @@ Methods:
8 map : Functor f => (func : a -> b) -> f a -> f b
8 map : Functor f => (func : a -> b) -> f a -> f b
9 Apply a function across everything of type 'a' in a parameterised type
9 Apply a function across everything of type 'a' in a parameterised type
10
10
11− The function is Total
11+ The function is: Total & public export
12Implementations:
12Implementations:
13 Functor (Pair a)
13 Functor (Pair a)
14 Functor List
14 Functor List
@@ -33,7 +33,9 @@ Named implementation:
33 docs003.mine : Functor List
33 docs003.mine : Functor List
34
34
35
35
36+ The function is: public export
36Named implementation:
37Named implementation:
37 docs003.another : Functor List
38 docs003.another : Functor List
38 More functors!
39 More functors!
39
40
41+ The function is: public export
test/docs004/expected+3−3
@@ -7,12 +7,12 @@ Main.MkFoo : (bar : Nat) -> (baz : Bool) -> Foo a
7
7
8 baz : Bool -- A field baz
8 baz : Bool -- A field baz
9
9
10− The function is Total
10+ The function is: Total & public export
11Main.Foo.bar : (rec : Foo a) -> Nat
11Main.Foo.bar : (rec : Foo a) -> Nat
12 A field bar
12 A field bar
13
13
14− The function is Total
14+ The function is: Total & public export
15Main.Foo.baz : (rec : Foo a) -> Bool
15Main.Foo.baz : (rec : Foo a) -> Bool
16 A field baz
16 A field baz
17
17
18− The function is Total
18+ The function is: Total & public export
test/docs005/expected+3−1
@@ -1,6 +1,7 @@
1Data type docs005.Foobar : Type
1Data type docs005.Foobar : Type
2 A foobar with an auto implicit
2 A foobar with an auto implicit
3
3
4+ The function is: public export
4Constructors:
5Constructors:
5 NewFoo : (xs : List String) ->
6 NewFoo : (xs : List String) ->
6 (ys : List Nat) -> {auto prf : NonEmpty ys} -> Foobar
7 (ys : List Nat) -> {auto prf : NonEmpty ys} -> Foobar
@@ -14,6 +15,7 @@ Constructors:
14
15
15 (auto implicit) prf : NonEmpty ys -- The prf
16 (auto implicit) prf : NonEmpty ys -- The prf
16
17
18+ The function is: public export
17docs005.NewFoo : (xs : List String) ->
19docs005.NewFoo : (xs : List String) ->
18 (ys : List Nat) -> {auto prf : NonEmpty ys} -> Foobar
20 (ys : List Nat) -> {auto prf : NonEmpty ys} -> Foobar
19 New Foo
21 New Foo
@@ -26,4 +28,4 @@ docs005.NewFoo : (xs : List String) ->
26
28
27 (auto implicit) prf : NonEmpty ys -- The prf
29 (auto implicit) prf : NonEmpty ys -- The prf
28
30
29− The function is Total
31+ The function is: Total & public export
test/docs006/expected+1−1
@@ -11,6 +11,6 @@ Methods:
11 m : Foo t => t
11 m : Foo t => t
12 member of interface
12 member of interface
13
13
14− The function is Total
14+ The function is: Total & public export
15Implementations:
15Implementations:
16 <no implementations>
16 <no implementations>
test/idrisdoc009/expected+2
@@ -1,10 +1,12 @@
1Data type Test.Test : Type
1Data type Test.Test : Type
2 Docs for datatype Test.
2 Docs for datatype Test.
3
3
4+ The function is: public export
4Constructors:
5Constructors:
5 MkTest : Test
6 MkTest : Test
6
7
7
8
9+ The function is: public export
8Module Test:
10Module Test:
9 Docs for module Test.
11 Docs for module Test.
10
12
test/interactive005/expected+3−3
@@ -3,7 +3,7 @@ Hello, World
3Main.main : IO ()
3Main.main : IO ()
4 This is a docstring
4 This is a docstring
5
5
6− The function is Total
6+ The function is: Total & public export
7Main.main is Total
7Main.main is Total
8Hello, World
8Hello, World
9id : a -> a
9id : a -> a
@@ -27,10 +27,10 @@ Main.main : IO ()
27 is a
27 is a
28 docstring
28 docstring
29
29
30− The function is Total
30+ The function is: Total & public export
31Main.main : IO ()
31Main.main : IO ()
32 This is a docstring
32 This is a docstring
33
33
34− The function is Total
34+ The function is: Total & public export
35Nat2 : Type
35Nat2 : Type
36Invalid filename for compiler output "Test.idr"
36Invalid filename for compiler output "Test.idr"
test/interfaces001/expected+3−2
@@ -8,7 +8,7 @@ Methods:
8 myShow : MyShow a => (x : a) -> String
8 myShow : MyShow a => (x : a) -> String
9 The shower
9 The shower
10
10
11− The function is Total
11+ The function is: Total & public export
12Implementation constructor:
12Implementation constructor:
13 MkMyShow : (myShow : a -> String) -> MyShow a
13 MkMyShow : (myShow : a -> String) -> MyShow a
14 Build a MyShow
14 Build a MyShow
@@ -17,6 +17,7 @@ Implementation constructor:
17
17
18 myShow : a -> String -- The shower
18 myShow : a -> String -- The shower
19
19
20+ The function is: public export
20Implementations:
21Implementations:
21 MyShow Integer
22 MyShow Integer
22MkMyShow : (myShow : a -> String) -> MyShow a
23MkMyShow : (myShow : a -> String) -> MyShow a
@@ -26,4 +27,4 @@ MkMyShow : (myShow : a -> String) -> MyShow a
26
27
27 myShow : a -> String -- The shower
28 myShow : a -> String -- The shower
28
29
29− The function is Total
30+ The function is: Total & public export