+ let_defs:[
+ [ defs = LIST1 [
+ name = IDENT;
+ args = LIST1 [
+ PAREN "(" ; names = LIST1 IDENT SEP SYMBOL ","; SYMBOL ":";
+ ty = term; PAREN ")" ->
+ (names, ty)
+ ];
+ index_name = OPT [ IDENT "on"; idx = IDENT -> idx ];
+ ty = OPT [ SYMBOL ":" ; t = term -> t ];
+ SYMBOL <:unicode<def>> (* ≝ *);
+ t1 = term ->
+ let rec list_of_binder binder ty final_term = function
+ | [] -> final_term
+ | name::tl ->
+ CicAst.Binder (binder, (Cic.Name name, Some ty),
+ list_of_binder binder ty final_term tl)
+ in
+ let rec binder_of_arg_list binder final_term = function
+ | [] -> final_term
+ | (l,ty)::tl ->
+ list_of_binder binder ty
+ (binder_of_arg_list binder final_term tl) l
+ in
+ let t1' = binder_of_arg_list `Lambda t1 args in
+ let ty' =
+ match ty with
+ | None -> None
+ | Some ty -> Some (binder_of_arg_list `Pi ty args)
+ in
+ let rec get_position_of name n = function
+ | [] -> (None,n)
+ | nam::tl ->
+ if nam = name then
+ (Some n,n)
+ else
+ (get_position_of name (n+1) tl)
+ in
+ let rec find_arg name n = function
+ | [] -> (fail loc (sprintf "Argument %s not found" name))
+ | (l,_)::tl ->
+ let (got,len) = get_position_of name 0 l in
+ (match got with
+ | None -> (find_arg name (n+len) tl)
+ | Some where -> n + where)
+ in
+ let index =
+ (match index_name with
+ | None -> 0
+ | (Some name) -> find_arg name 0 args)
+ in
+ ((Cic.Name name,ty'), t1', index)
+ ] SEP "and" -> defs
+ ]];