Ekdohibs
/
ocaml
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

prove functionality and associativity of plus 

git-svn-id: http://caml.inria.fr/svn/ocaml/trunk@12486 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02
master
Jacques Garrigue 2012-05-26 01:25:42 +00:00
parent 1253a7c689
commit 6d950dd3ea
2 changed files with 12 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
testsuite/tests/typing-gadts/omega07.ml.principal.reference
View File

@ -54,6 +54,12 @@ val even4 : four even = EvenSS (EvenSS EvenZ)
# type (_, _) equal = Eq : ('a, 'a) equal
val convert : ('a, 'b) equal -> 'a -> 'b = <fun>
val sameNat : 'a nat -> 'b nat -> ('a, 'b) equal option = <fun>
# val plus_func : ('a, 'b, 'm) plus -> ('a, 'b, 'n) plus -> ('m, 'n) equal =
<fun>
val plus_assoc :
('a, 'b, 'ab) plus ->
('ab, 'c, 'm) plus ->
('b, 'c, 'bc) plus -> ('a, 'bc, 'n) plus -> ('m, 'n) equal = <fun>
# val smaller : ('a succ, 'b succ) le -> ('a, 'b) le = <fun>
# type (_, _) diff = Diff : 'c nat * ('a, 'c, 'b) plus -> ('a, 'b) diff
# * * * * * * * * * val diff : ('a, 'b) le -> 'a nat -> 'b nat -> ('a, 'b) diff = <fun>

6
testsuite/tests/typing-gadts/omega07.ml.reference
View File

@ -54,6 +54,12 @@ val even4 : four even = EvenSS (EvenSS EvenZ)
# type (_, _) equal = Eq : ('a, 'a) equal
val convert : ('a, 'b) equal -> 'a -> 'b = <fun>
val sameNat : 'a nat -> 'b nat -> ('a, 'b) equal option = <fun>
# val plus_func : ('a, 'b, 'm) plus -> ('a, 'b, 'n) plus -> ('m, 'n) equal =
<fun>
val plus_assoc :
('a, 'b, 'ab) plus ->
('ab, 'c, 'm) plus ->
('b, 'c, 'bc) plus -> ('a, 'bc, 'n) plus -> ('m, 'n) equal = <fun>
# val smaller : ('a succ, 'b succ) le -> ('a, 'b) le = <fun>
# type (_, _) diff = Diff : 'c nat * ('a, 'c, 'b) plus -> ('a, 'b) diff
# * * * * * * * * * val diff : ('a, 'b) le -> 'a nat -> 'b nat -> ('a, 'b) diff = <fun>