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

   1 module T = RecommTypes
   2 module R = RecommCheck
   3 module D = RecommGcsAttr
   4
   5 let step k st outs ins =
   6   if st = T.KO then k st outs ins else
   7   match ins with
   8   | "iterators" :: tl -> k T.OK ("iterators" :: outs) tl
   9   | "eliminations" :: tl -> k T.OK ("eliminations" :: outs) tl
  10   | "eliminators" :: tl -> k T.OK ("eliminations" :: outs) tl
  11   | "equalities" :: tl -> k T.OK ("equalities" :: outs) tl
  12   | "destructions" :: tl -> k T.OK ("destructions" :: outs) tl
  13   | "forward" :: "properties" :: tl -> k T.OK ("destructions" :: outs) tl
  14   | "forward" :: "lemmas" :: tl -> k T.OK ("destructions" :: outs) tl
  15   | "inversions" :: tl -> k T.OK ("inversions" :: outs) tl
  16   | "inversion" :: "properties" :: tl -> k T.OK ("inversions" :: outs) tl
  17   | "inversion" :: "lemmas" :: tl -> k T.OK ("inversions" :: outs) tl
  18   | "inversion" :: tl -> k T.OK ("inversions" :: outs) tl
  19   | "constructions" :: tl -> k T.OK ("constructions" :: outs) tl
  20   | "properties" :: tl -> k T.OK ("constructions" :: outs) tl
  21   | _ -> k T.KO outs ins
  22
  23 let main =
  24   R.register_s step