matita/matita/contribs/lambdadelta/bin/recomm/recommGcrGroundArith.ml

   1 module T = RecommTypes
   2 module R = RecommPccFor
   3
   4 let step k st outs ins =
   5   if st <> T.OO then k st outs ins else
   6   match ins with
   7   | "ARITHMETICAL" :: "PROPERTIES" :: tl -> k T.OK ("PROPERTIES" :: "ARITHMETICAL" :: outs) tl
   8   | "STRICT" :: "ORDER" :: tl -> k T.OK ("ORDER" :: "STRICT" :: outs) tl
   9   | "ORDER" :: tl -> k T.OK ("ORDER" :: outs) tl
  10   | "MAXIMUM" :: tl -> k T.OK ("MAXIMUM" :: outs) tl
  11   | "LEFT" :: "SUBTRACTION" :: tl -> k T.OK ("SUBTRACTION" :: "LEFT" :: outs) tl
  12   | "SUBTRACTION" :: tl -> k T.OK ("SUBTRACTION" :: outs) tl
  13   | "ADDITION" :: tl -> k T.OK ("ADDITION" :: outs) tl
  14   | "RIGHT" :: "ADDITION" :: tl -> k T.OK ("ADDITION" :: "RIGHT" :: outs) tl
  15   | "PREDECESSOR" :: tl -> k T.OK ("PREDECESSOR" :: outs) tl
  16   | "SUCCESSOR" :: tl -> k T.OK ("SUCCESSOR" :: outs) tl
  17   | "NAT-INJECTION" :: tl -> k T.OK ("NAT-INJECTION" :: outs) tl
  18   | "TRICHOTOMY" :: "OPERATOR" :: tl -> k T.OK ("OPERATOR" :: "TRICHOTOMY" :: outs) tl
  19   | "ITERATED" :: "FUNCTION" :: tl -> k T.OK ("FUNCTION" :: "ITERATED" :: outs) tl
  20   | "DISCRIMINATOR" :: tl -> k T.OK ("DISCRIMINATOR" :: outs) tl
  21   | _ -> k T.OO outs ins
  22
  23 let main =
  24   R.register_r step