Update REPL :doc related tests with totality status
commit164c4f6a27b5e7ddd3fba886966f8724f6f7d50b
authorGuglielmo Fachini <guglielmo@fachini.net>
dateSat 13 Jun 2015, 16:10 (11 years ago)
parent0922ca1
test/classes001/expected+2
@@ -8,6 +8,7 @@ Methods:
88 myShow : MyShow a => (x : a) -> String
99 The shower
1010
11+ The function is Total
1112Instance constructor:
1213 MkMyShow : (myShow : a -> String) -> MyShow a
1314 Build a MyShow
@@ -25,3 +26,4 @@ MkMyShow : (myShow : a -> String) -> MyShow a
2526
2627 myShow : a -> String -- The shower
2728
29+ The function is Total
test/docs001/expected+1
@@ -8,6 +8,7 @@ Methods:
88 m : C t => t
99 member of class
1010
11+ The function is Total
1112Instances:
1213 C A
1314 instance of class
test/docs002/expected+3
@@ -1,9 +1,12 @@
11T1 : Type
22 Some documentation
33
4+ The function is Total
45T2 : Type
56 Some other documentation
67
8+ The function is Total
79T3 : Int
810 Some provided postulate
911
12+ The function is not yet checked for totality
test/docs003/expected+1
@@ -8,6 +8,7 @@ Methods:
88 map : Functor f => (m : a -> b) -> f a -> f b
99 The action of the functor on morphisms
1010
11+ The function is Total
1112Instances:
1213 Functor List
1314 Functor Stream
test/docs004/expected+3
@@ -7,9 +7,12 @@ MkFoo : (bar : Nat) -> (baz : Bool) -> Foo a
77
88 baz : Bool -- A field baz
99
10+ The function is Total
1011bar : (rec : Foo a) -> Nat
1112 A field bar
1213
14+ The function is Total
1315baz : (rec : Foo a) -> Bool
1416 A field baz
1517
18+ The function is Total
test/interactive005/expected+3
@@ -3,6 +3,7 @@ Hello, World
33main : IO ()
44 This is a docstring
55
6+ The function is Total
67Main.main is Total
78Hello, World
89Prelude.Basics.id : a -> a
@@ -26,8 +27,10 @@ main : IO ()
2627 is a
2728 docstring
2829
30+ The function is Total
2931main : IO ()
3032 This is a docstring
3133
34+ The function is Total
3235Nat2 : Type
3336Invalid filename for compiler output "Test.idr"