let op, cp = if p then "(", ")" else "", "" in
let a = R.alpha B.mem e a in
let ee = B.push e B.empty a (B.abst n w) in
- let binder = match N.to_string st n with
- | "1" -> "Π"
- | "2" -> "λ"
- | _ -> ok := false; "?"
+ let binder = match N.to_string st n, a.E.n_sort with
+ | "1", 0 -> "Π"
+ | "1", 1 -> "∀"
+ | "2", _ -> "λ"
+ | _ -> ok := false; "?"
in
P.fprintf och "%s%s%a:%a.%a%s"
op binder out_name a (out_term st false e) w (out_term st false ee) t cp
let path = F.concat dir fname in
let och = open_out (path ^ ext) in
out_preamble och;
- out_top_comment och (P.sprintf "This file is generated by %s: do not edit" G.version_string);
+ out_top_comment och (P.sprintf "This file was generated by %s: do not edit" G.version_string);
out_include och "basics/pts";
och
let output_entity st och (_, na, s, b) =
- let f i =
- out_comment och (P.sprintf "notion %u" i);
- match b with
- | E.Abbr t ->
- P.fprintf och "definition %a ≝ %a.\n\n%!" out_uri s (out_term st false B.empty) t; !ok
- | E.Abst t ->
- P.fprintf och "axiom %a : %a.\n\n%!" out_uri s (out_term st false B.empty) t; !ok
- | E.Void -> C.err ()
- in
- E.apix C.err f na
+ out_comment och (P.sprintf "constant %u" na.E.n_apix);
+ match b with
+ | E.Abbr t ->
+ P.fprintf och "definition %a ≝ %a.\n\n%!" out_uri s (out_term st false B.empty) t; !ok
+ | E.Abst t ->
+ P.fprintf och "axiom %a : %a.\n\n%!" out_uri s (out_term st false B.empty) t; !ok
+ | E.Void -> C.err ()
let close_out och = close_out och