ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-11-13 07:26:59 +03:00
Code Issues Projects Releases Wiki Activity

Update REPL :doc related tests with totality status

Browse Source
This commit is contained in:
Guglielmo Fachini 2015-06-13 16:10:25 +02:00
parent 0922ca11a8
commit 164c4f6a27
6 changed files with 13 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
test/classes001/expected
View File

@ -8,6 +8,7 @@ Methods:
myShow : MyShow a => (x : a) -> String
The shower
The function is Total
Instance constructor:
MkMyShow : (myShow : a -> String) -> MyShow a
Build a MyShow
@ -25,3 +26,4 @@ MkMyShow : (myShow : a -> String) -> MyShow a
myShow : a -> String -- The shower
The function is Total

1
test/docs001/expected
View File

@ -8,6 +8,7 @@ Methods:
m : C t => t
member of class
The function is Total
Instances:
C A
instance of class

3
test/docs002/expected
View File

@ -1,9 +1,12 @@
T1 : Type
Some documentation
The function is Total
T2 : Type
Some other documentation
The function is Total
T3 : Int
Some provided postulate
The function is not yet checked for totality

1
test/docs003/expected
View File

@ -8,6 +8,7 @@ Methods:
map : Functor f => (m : a -> b) -> f a -> f b
The action of the functor on morphisms
The function is Total
Instances:
Functor List
Functor Stream

3
test/docs004/expected
View File

@ -7,9 +7,12 @@ MkFoo : (bar : Nat) -> (baz : Bool) -> Foo a
baz : Bool -- A field baz
The function is Total
bar : (rec : Foo a) -> Nat
A field bar
The function is Total
baz : (rec : Foo a) -> Bool
A field baz
The function is Total

3
test/interactive005/expected
View File

@ -3,6 +3,7 @@ Hello, World
main : IO ()
This is a docstring
The function is Total
Main.main is Total
Hello, World
Prelude.Basics.id : a -> a
@ -26,8 +27,10 @@ main : IO ()
is a
docstring
The function is Total
main : IO ()
This is a docstring
The function is Total
Nat2 : Type
Invalid filename for compiler output "Test.idr"