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

diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcbGroundArith.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcbGroundArith.ml
new file mode 100644
index 000000000..1528eb2b1
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcbGroundArith.ml
@@ -0,0 +1,26 @@
+module T = RecommTypes
+module R = RecommPcsAnd
+
+let step k st outs ins =
+  if st <> T.OO then k st outs ins else
+  match ins with
+  | "ylt" :: tl -> k T.OK ("ylt" :: outs) tl
+  | "yle" :: tl -> k T.OK ("yle" :: outs) tl
+  | "ylminus" :: tl -> k T.OK ("ylminus" :: outs) tl
+  | "yminus" :: tl -> k T.OK ("ylminus" :: outs) tl
+  | "yplus" :: tl -> k T.OK ("yplus" :: outs) tl
+  | "ypred" :: tl -> k T.OK ("ypred" :: outs) tl
+  | "ysucc" :: tl -> k T.OK ("ysucc" :: outs) tl
+  | "nlt" :: tl -> k T.OK ("nlt" :: outs) tl
+  | "nle" :: tl -> k T.OK ("nle" :: outs) tl
+  | "nmax" :: tl -> k T.OK ("nmax" :: outs) tl
+  | "nminus" :: tl -> k T.OK ("nminus" :: outs) tl
+  | "nplus" :: tl -> k T.OK ("nplus" :: outs) tl
+  | "npred" :: tl -> k T.OK ("npred" :: outs) tl
+  | "nsucc" :: tl -> k T.OK ("nsucc" :: outs) tl
+  | "ntri" :: tl -> k T.OK ("ntri" :: outs) tl
+  | "niter" :: tl -> k T.OK ("niter" :: outs) tl
+  | _ -> k T.OO outs ins
+
+let main =
+  R.register_b step