Mizarlight/pa_f.ml

   1 (* ------------------------------------------------------------------------- *)
   2 (* Some additional infixes to support Freek's "Mizar Light".                 *)
   3 (* ------------------------------------------------------------------------- *)
   4
   5 open Pcaml;
   6
   7 Pcaml.syntax_name.val := "Freek";
   8
   9 Format.print_string "New infixes set up";
  10 Format.print_newline();
  11
  12 EXTEND
  13   expr: AFTER "<"
  14    [[ f = expr; "by"; g = expr -> <:expr< ((by $f$) $g$) >>
  15     | f = expr; "st'"; g = expr -> <:expr< ((st' $f$) $g$) >>
  16     | f = expr; "st"; g = expr -> <:expr< ((st $f$) $g$) >>
  17     | f = expr; "at"; g = expr -> <:expr< ((at $f$) $g$) >>
  18     | f = expr; "from"; g = expr -> <:expr< ((from $f$) $g$) >>
  19     | f = expr; "using"; g = expr -> <:expr< ((using $f$) $g$) >>
  20     | f = expr; "proof"; g = expr -> <:expr< ((proof $f$) $g$) >>
  21     | f = expr; "THEN'"; g = expr -> <:expr< ((then'_ $f$) $g$) >>
  22
  23    ]];
  24
  25 END;