+ | Ast.LetRec (kind, definitions, (source, flavour, _)) ->
+ let rec get_guard i = function
+ | [] -> assert false (* Ast.Implicit `JustOne *)
+ | [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 -> assert false (* Ast.Implicit `JustOne *)
+ | Some typ -> typ
+ in
+ sprintf "%s %s on %s: %s \\def %s"
+ (pp_term id)
+ (String.concat " " (List.map (pp_capture_variable pp_term) params))
+ (pp_term (get_guard i params))
+ (pp_term typ) (pp_term body)
+ in
+ sprintf "%s%s %s %s"
+ (string_of_source source)
+ (match kind with `Inductive -> "rec" | `CoInductive -> "corec")
+ (NCicPp.string_of_flavour flavour)
+ (String.concat " and " (List.map map definitions))