X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbin%2Frecomm%2FrecommGcrGroundArith.ml;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbin%2Frecomm%2FrecommGcrGroundArith.ml;h=091cc7f5f52e8fa2433cba677e18840549a66972;hb=4d232392091ee233afc26ecf3120dd5f5c6a33c8;hp=0000000000000000000000000000000000000000;hpb=da0775e27b362e91ea1453a800bc403781cc2ca3;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcrGroundArith.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcrGroundArith.ml
new file mode 100644
index 000000000..091cc7f5f
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcrGroundArith.ml
@@ -0,0 +1,24 @@
+module T = RecommTypes
+module R = RecommPccFor
+
+let step k st outs ins =
+  if st <> T.OO then k st outs ins else
+  match ins with
+  | "ARITHMETICAL" :: "PROPERTIES" :: tl -> k T.OK ("PROPERTIES" :: "ARITHMETICAL" :: outs) tl
+  | "STRICT" :: "ORDER" :: tl -> k T.OK ("ORDER" :: "STRICT" :: outs) tl
+  | "ORDER" :: tl -> k T.OK ("ORDER" :: outs) tl
+  | "MAXIMUM" :: tl -> k T.OK ("MAXIMUM" :: outs) tl
+  | "MAXIMUN" :: tl -> k T.OK ("MAXIMUM" :: outs) tl
+  | "LEFT" :: "SUBTRACTION" :: tl -> k T.OK ("SUBTRACTION" :: "LEFT" :: outs) tl
+  | "SUBTRACTION" :: tl -> k T.OK ("SUBTRACTION" :: outs) tl
+  | "ADDITION" :: tl -> k T.OK ("ADDITION" :: outs) tl
+  | "PREDECESSOR" :: tl -> k T.OK ("PREDECESSOR" :: outs) tl
+  | "SUCCESSOR" :: tl -> k T.OK ("SUCCESSOR" :: outs) tl
+  | "NAT-INJECTION" :: tl -> k T.OK ("NAT-INJECTION" :: outs) tl
+  | "TRICHOTOMY" :: "OPERATOR" :: tl -> k T.OK ("OPERATOR" :: "TRICHOTOMY" :: outs) tl
+  | "ITERATED" :: "FUNCTION" :: tl -> k T.OK ("FUNCTION" :: "ITERATED" :: outs) tl
+  | "DISCRIMINATOR" :: tl -> k T.OK ("DISCRIMINATOR" :: outs) tl
+  | _ -> k T.OO outs ins
+
+let main =
+  R.register_r step