git.iko.soy/Idris-dev
on master help sign in
Amended the test suite to report updated documentation.
commit8fe28aa1634929cf427bc762a3e973801dd22bb5 authorJan de Muijnck-Hughes <jan.deMuijnck-Hughes@glasgow.ac.uk> dateWed 15 May 2019, 13:47 (7 years ago) parent36bcf4b
9 files changed+22−15
compare with master
unifiedsplit
test/docs001/expected+1−1 test/docs002/expected+3−3 test/docs003/expected+3−1 test/docs004/expected+3−3 test/docs005/expected+3−1 test/docs006/expected+1−1 test/idrisdoc009/expected+2 test/interactive005/expected+3−3 test/interfaces001/expected+3−2
test/docs001/expected+1−1
@@ -8,7 +8,7 @@ Methods:
88 m : C t => t
99 member of interface
1010
11− The function is Total
11+ The function is: Total & public export
1212Implementations:
1313 C A
1414 implementation of interface
test/docs002/expected+3−3
@@ -1,12 +1,12 @@
11T1 : Type
22 Some documentation
33
4− The function is Total
4+ The function is: Total & public export
55T2 : Type
66 Some other documentation
77
8− The function is Total
8+ The function is: Total & public export
99T3 : Int
1010 Some provided postulate
1111
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:
88 map : Functor f => (func : a -> b) -> f a -> f b
99 Apply a function across everything of type 'a' in a parameterised type
1010
11− The function is Total
11+ The function is: Total & public export
1212Implementations:
1313 Functor (Pair a)
1414 Functor List
@@ -33,7 +33,9 @@ Named implementation:
3333 docs003.mine : Functor List
3434
3535
36+ The function is: public export
3637Named implementation:
3738 docs003.another : Functor List
3839 More functors!
3940
41+ The function is: public export
test/docs004/expected+3−3
@@ -7,12 +7,12 @@ Main.MkFoo : (bar : Nat) -> (baz : Bool) -> Foo a
77
88 baz : Bool -- A field baz
99
10− The function is Total
10+ The function is: Total & public export
1111Main.Foo.bar : (rec : Foo a) -> Nat
1212 A field bar
1313
14− The function is Total
14+ The function is: Total & public export
1515Main.Foo.baz : (rec : Foo a) -> Bool
1616 A field baz
1717
18− The function is Total
18+ The function is: Total & public export
test/docs005/expected+3−1
@@ -1,6 +1,7 @@
11Data type docs005.Foobar : Type
22 A foobar with an auto implicit
33
4+ The function is: public export
45Constructors:
56 NewFoo : (xs : List String) ->
67 (ys : List Nat) -> {auto prf : NonEmpty ys} -> Foobar
@@ -14,6 +15,7 @@ Constructors:
1415
1516 (auto implicit) prf : NonEmpty ys -- The prf
1617
18+ The function is: public export
1719docs005.NewFoo : (xs : List String) ->
1820 (ys : List Nat) -> {auto prf : NonEmpty ys} -> Foobar
1921 New Foo
@@ -26,4 +28,4 @@ docs005.NewFoo : (xs : List String) ->
2628
2729 (auto implicit) prf : NonEmpty ys -- The prf
2830
29− The function is Total
31+ The function is: Total & public export
test/docs006/expected+1−1
@@ -11,6 +11,6 @@ Methods:
1111 m : Foo t => t
1212 member of interface
1313
14− The function is Total
14+ The function is: Total & public export
1515Implementations:
1616 <no implementations>
test/idrisdoc009/expected+2
@@ -1,10 +1,12 @@
11Data type Test.Test : Type
22 Docs for datatype Test.
33
4+ The function is: public export
45Constructors:
56 MkTest : Test
67
78
9+ The function is: public export
810Module Test:
911 Docs for module Test.
1012
test/interactive005/expected+3−3
@@ -3,7 +3,7 @@ Hello, World
33Main.main : IO ()
44 This is a docstring
55
6− The function is Total
6+ The function is: Total & public export
77Main.main is Total
88Hello, World
99id : a -> a
@@ -27,10 +27,10 @@ Main.main : IO ()
2727 is a
2828 docstring
2929
30− The function is Total
30+ The function is: Total & public export
3131Main.main : IO ()
3232 This is a docstring
3333
34− The function is Total
34+ The function is: Total & public export
3535Nat2 : Type
3636Invalid filename for compiler output "Test.idr"
test/interfaces001/expected+3−2
@@ -8,7 +8,7 @@ Methods:
88 myShow : MyShow a => (x : a) -> String
99 The shower
1010
11− The function is Total
11+ The function is: Total & public export
1212Implementation constructor:
1313 MkMyShow : (myShow : a -> String) -> MyShow a
1414 Build a MyShow
@@ -17,6 +17,7 @@ Implementation constructor:
1717
1818 myShow : a -> String -- The shower
1919
20+ The function is: public export
2021Implementations:
2122 MyShow Integer
2223MkMyShow : (myShow : a -> String) -> MyShow a
@@ -26,4 +27,4 @@ MkMyShow : (myShow : a -> String) -> MyShow a
2627
2728 myShow : a -> String -- The shower
2829
29− The function is Total
30+ The function is: Total & public export