\forall n:nat. n > 0 \or n = 0
is parsed "correctly"
return_term loc
(CicAst.Binder (`Pi, (Cic.Anonymous, Some t1), t2))
]
return_term loc
(CicAst.Binder (`Pi, (Cic.Anonymous, Some t1), t2))
]
+ | "logic_add" LEFTA [ (* nothing here by default *) ]
+ | "logic_mult" LEFTA [ (* nothing here by default *) ]
+ | "logic_inv" NONA [ (* nothing here by default *) ]
| "relop" LEFTA
[ t1 = term; SYMBOL "="; t2 = term ->
return_term loc (CicAst.Appl [CicAst.Symbol ("eq", 0); t1; t2])
| "relop" LEFTA
[ t1 = term; SYMBOL "="; t2 = term ->
return_term loc (CicAst.Appl [CicAst.Symbol ("eq", 0); t1; t2])
open CicTextualParser2
EXTEND
open CicTextualParser2
EXTEND
+ term: LEVEL "logic_add"
[
[ t1 = term; SYMBOL <:unicode<lor>> (* ∨ *); t2 = term ->
return_term loc (CicAst.Appl [CicAst.Symbol ("or", 0); t1; t2])
]
];
[
[ t1 = term; SYMBOL <:unicode<lor>> (* ∨ *); t2 = term ->
return_term loc (CicAst.Appl [CicAst.Symbol ("or", 0); t1; t2])
]
];
+ term: LEVEL "logic_mult"
[
[ t1 = term; SYMBOL <:unicode<land>> (* ∧ *); t2 = term ->
return_term loc (CicAst.Appl [CicAst.Symbol ("and", 0); t1; t2])
]
];
[
[ t1 = term; SYMBOL <:unicode<land>> (* ∧ *); t2 = term ->
return_term loc (CicAst.Appl [CicAst.Symbol ("and", 0); t1; t2])
]
];
+ term: LEVEL "logic_inv"
[
[ SYMBOL <:unicode<lnot>> (* ¬ *); t = term ->
return_term loc (CicAst.Appl [CicAst.Symbol ("not", 0); t])
[
[ SYMBOL <:unicode<lnot>> (* ¬ *); t = term ->
return_term loc (CicAst.Appl [CicAst.Symbol ("not", 0); t])