branch for universe

[helm.git] / matita / contribs / assembly / freescale / freescale_ocaml / matita_datatypes_compare.ml

diff --git a/matita/contribs/assembly/freescale/freescale_ocaml/matita_datatypes_compare.ml b/matita/contribs/assembly/freescale/freescale_ocaml/matita_datatypes_compare.ml
new file mode 100644 (file)
index 0000000..66e19cd
--- /dev/null
+++ b/matita/contribs/assembly/freescale/freescale_ocaml/matita_datatypes_compare.ml
@@ -0,0 +1,33 @@
+type compare =
+LT
+ | EQ
+ | GT
+;;
+
+let compare_rec =
+(function p -> (function p1 -> (function p2 -> (function c -> 
+(match c with 
+   LT -> p
+ | EQ -> p1
+ | GT -> p2)
+))))
+;;
+
+let compare_rect =
+(function p -> (function p1 -> (function p2 -> (function c -> 
+(match c with 
+   LT -> p
+ | EQ -> p1
+ | GT -> p2)
+))))
+;;
+
+let compare_invert =
+(function c -> 
+(match c with 
+   LT -> GT
+ | EQ -> EQ
+ | GT -> LT)
+)
+;;
+