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

   1 module D = RecommGcsAttr
   2
   3 let step k ok outs ins =
   4   if ok then k ok outs ins else
   5   match ins with
   6   | "eliminations" :: tl -> k ok ("eliminations" :: outs) tl
   7   | "eliminators" :: tl -> k ok ("eliminations" :: outs) tl
   8   | "destructions" :: tl -> k ok ("destructions" :: outs) tl
   9   | "forward" :: "properties" :: tl -> k ok ("destructions" :: outs) tl
  10   | "forward" :: "lemmas" :: tl -> k ok ("destructions" :: outs) tl
  11   | "inversions" :: tl -> k ok ("inversions" :: outs) tl
  12   | "inversion" :: "properties" :: tl -> k ok ("inversions" :: outs) tl
  13   | "inversion" :: "lemmas" :: tl -> k ok ("inversions" :: outs) tl
  14   | "constructions" :: tl -> k ok ("constructions" :: outs) tl
  15   | "properties" :: tl -> k ok ("constructions" :: outs) tl
  16   | _ -> k true outs ins
  17
  18 let main =
  19   RecommCheck.register_s step