1 (((((((v (((a v) w) (((a v) w) v))) (w. c)) (b (a v))) c) (z. a)) (x. (w. (w. c)))) (((a (y c)) ((y c) ((a v) (w (z. a))))) (w. c)))
\r
2 ((((((v (((a v) w) (((a v) w) v))) (w. c)) (b (a v))) c) (z. a)) (x. (w. (w. c))))
\r
3 (((((b (a v)) (a. (y c))) z) (w. w)) ((a c) c))
\r
4 (((((v (((a v) w) (((a v) w) v))) (w. c)) (b (a v))) c) (z. a))
\r
5 ((((a (y c)) ((y c) ((a v) (w (z. a))))) (w. c)) (x. w))
\r
20 let fancy_of_term : nf -> Console.fancyobj =
\r
22 let of_var level n =
\r
24 then fancy_of_string (string_of_var n)
\r
25 else (("x" ^ string_of_int (level-n-1)) / ("var<sup>" ^ string_of_int (n-level) ^ "</sup>"))
\r
26 in let rec aux level = function
\r
27 `Var n -> of_var level n
\r
28 | `N n -> fancy_of_string (string_of_int n)
\r
29 | `Match(t,bs_lift,bs,args) ->
\r
30 "([" ^^ aux level (t :> nf) ^^
\r
31 " ? " ^ String.concat " | " (List.map (fun (n,t) -> string_of_int n ^ " => " ^ print ~l (lift bs_lift t)) !bs) ^ "] " ^
\r
32 String.concat " " (List.map (print ~l) args) ^ ")"
\r
33 | `I(n,args) -> "(" ^ print_name l n ^ " " ^ String.concat " " (Listx.to_list (Listx.map (print ~l) args)) ^ ")"
\r
35 let name = string_of_var (List.length l) in
\r
36 "λ" ^ name ^ "." ^ print ~l:(name::l) (nf : nf)
\r