[ defs = LIST1 [
name = IDENT;
args = LIST1 [
- PAREN "(" ; names = LIST1 IDENT SEP SYMBOL ","; SYMBOL ":";
- ty = term; PAREN ")" ->
- (names, ty)
+ PAREN "(" ; names = LIST1 IDENT SEP SYMBOL ",";
+ SYMBOL ":"; ty = term; PAREN ")" ->
+ (names, Some ty)
+ | name = IDENT -> [name],None
];
index_name = OPT [ IDENT "on"; idx = IDENT -> idx ];
ty = OPT [ SYMBOL ":" ; t = term -> t ];
list_of_binder binder ty
(binder_of_arg_list binder final_term tl) l
in
+ let args =
+ List.map
+ (function
+ names,Some ty -> names,ty
+ | names,None -> names,CicAst.Implicit
+ ) args in
let t1' = binder_of_arg_list `Lambda t1 args in
let ty' =
match ty with