- let strip i t =
- let rec aux i l = function
- | Ast.Binder (_, var, body) when i > 0 -> aux (pred i) (var :: l) body
- | body -> List.rev l, body
- in
- aux i [] t
- in
- let map (var, body, i) =
- let id, vars, typ, body = match var with
- | term, Some typ ->
- let pvars, pbody = strip i typ in
- let _, bbody = strip i body in
- term, pvars, pbody, bbody
- | _ -> assert false
- in
- sprintf "%s %s: %s \\def %s"
+ let rec get_guard i = function
+ | [] -> (*assert false*) Ast.Implicit
+ | [term, _] when i = 1 -> term
+ | _ :: tl -> get_guard (pred i) tl
+ in
+ let map (params, (id,typ), body, i) =
+ let typ =
+ match typ with
+ None -> Ast.Implicit
+ | Some typ -> typ
+ in
+ sprintf "%s %s on %s: %s \\def %s"