git.iko.soy/Idris-dev
on master help sign in
Update REPL :doc related tests with totality status
164c4f6Guglielmo Fachini
test/classes001/expected+2
compare with master
unifiedsplit
@@ -8,6 +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
11Instance constructor:
12Instance constructor:
12 MkMyShow : (myShow : a -> String) -> MyShow a
13 MkMyShow : (myShow : a -> String) -> MyShow a
13 Build a MyShow
14 Build a MyShow
@@ -25,3 +26,4 @@ MkMyShow : (myShow : a -> String) -> MyShow a
25
26
26 myShow : a -> String -- The shower
27 myShow : a -> String -- The shower
27
28
29+ The function is Total
test/docs001/expected+1
@@ -8,6 +8,7 @@ Methods:
8 m : C t => t
8 m : C t => t
9 member of class
9 member of class
10
10
11+ The function is Total
11Instances:
12Instances:
12 C A
13 C A
13 instance of class
14 instance of class
test/docs002/expected+3
@@ -1,9 +1,12 @@
1T1 : Type
1T1 : Type
2 Some documentation
2 Some documentation
3
3
4+ The function is Total
4T2 : Type
5T2 : Type
5 Some other documentation
6 Some other documentation
6
7
8+ The function is Total
7T3 : Int
9T3 : Int
8 Some provided postulate
10 Some provided postulate
9
11
12+ The function is not yet checked for totality
test/docs003/expected+1
@@ -8,6 +8,7 @@ Methods:
8 map : Functor f => (m : a -> b) -> f a -> f b
8 map : Functor f => (m : a -> b) -> f a -> f b
9 The action of the functor on morphisms
9 The action of the functor on morphisms
10
10
11+ The function is Total
11Instances:
12Instances:
12 Functor List
13 Functor List
13 Functor Stream
14 Functor Stream
test/docs004/expected+3
@@ -7,9 +7,12 @@ 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
10bar : (rec : Foo a) -> Nat
11bar : (rec : Foo a) -> Nat
11 A field bar
12 A field bar
12
13
14+ The function is Total
13baz : (rec : Foo a) -> Bool
15baz : (rec : Foo a) -> Bool
14 A field baz
16 A field baz
15
17
18+ The function is Total
test/interactive005/expected+3
@@ -3,6 +3,7 @@ Hello, World
3main : IO ()
3main : IO ()
4 This is a docstring
4 This is a docstring
5
5
6+ The function is Total
6Main.main is Total
7Main.main is Total
7Hello, World
8Hello, World
8Prelude.Basics.id : a -> a
9Prelude.Basics.id : a -> a
@@ -26,8 +27,10 @@ main : IO ()
26 is a
27 is a
27 docstring
28 docstring
28
29
30+ The function is Total
29main : IO ()
31main : IO ()
30 This is a docstring
32 This is a docstring
31
33
34+ The function is Total
32Nat2 : Type
35Nat2 : Type
33Invalid filename for compiler output "Test.idr"
36Invalid filename for compiler output "Test.idr"