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])
]
| "add" LEFTA [ (* nothing here by default *) ]
| "mult" LEFTA [ (* nothing here by default *) ]
- | "power" LEFTA [ (* nothing here by default *) ]
+ | "power" LEFTA [ (* nothing here by default *) ]
| "inv" NONA [ (* nothing here by default *) ]
| "simple" NONA
[ sort = sort -> CicAst.Sort sort