helm/ocaml/cic_disambiguation/logic_notation.ml

   1 open Ast
   2 open Parser
   3
   4 EXTEND
   5   term: LEVEL "add"
   6     [
   7       [ t1 = term; SYMBOL "∨"; t2 = term ->
   8           return_term loc (Appl [Ident ("or", []); t1; t2])
   9       ]
  10     ];
  11   term: LEVEL "mult"
  12     [
  13       [ t1 = term; SYMBOL "∧"; t2 = term ->
  14         return_term loc (Appl [Ident ("and", []); t1; t2])
  15       ]
  16     ];
  17   term: LEVEL "inv"
  18     [
  19       [ SYMBOL "¬"; t = term ->
  20         return_term loc (Appl [Ident ("not", []); t])
  21       ]
  22     ];
  23 END