- | Set (_, name, value) -> sprintf "Set \"%s\" \"%s\"" name value
- | Inductive (_, params, types) ->
- let pp_constructors constructors =
- String.concat "\n"
- (List.map (fun (name, typ) -> sprintf "| %s: %s" name (pp_term_ast typ))
- constructors)
- in
- let pp_type (name, _, typ, constructors) =
- sprintf "\nwith %s: %s \\def\n%s" name (pp_term_ast typ)
- (pp_constructors constructors)
- in
- (match types with
- | [] -> assert false
- | (name, inductive, typ, constructors) :: tl ->
- let fst_typ_pp =
- sprintf "%sinductive %s%s: %s \\def\n%s"
- (if inductive then "" else "co") name (pp_params params)
- (pp_term_ast typ) (pp_constructors constructors)
- in
- fst_typ_pp ^ String.concat "" (List.map pp_type tl))
- | Theorem (_, flavour, name, typ, body) ->
- sprintf "%s %s: %s %s"
- (pp_flavour flavour)
- (match name with None -> "" | Some name -> name)
- (pp_term_ast typ)
- (match body with
- | None -> ""
- | Some body -> "\\def " ^ pp_term_ast body)
- | Coercion (_,_) -> "Coercion IMPLEMENT ME!!!!!"
+ | Drop _ -> "drop"
+ | Set (_, name, value) -> sprintf "set \"%s\" \"%s\"" name value
+ | Coercion (_,term) -> sprintf "coercion %s" (pp_term_ast term)