defs = let_defs; "in"; body = term ->
return_term loc (CicAst.LetRec (ind_kind, defs, body))
]
+ | "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 *) ]
+ | "inv" NONA [ (* nothing here by default *) ]
| "apply" LEFTA
[ t1 = term; t2 = term ->
let rec aux = function
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 *) ]
- | "inv" NONA [ (* nothing here by default *) ]
| "simple" NONA
[ sort = sort -> CicAst.Sort sort
| n = substituted_name -> return_term loc n