- | D.Abst x -> pp_terms "[:" "]" out x
- | D.Abbr x -> pp_terms "[=" "]" out x
- | D.Void x -> out (P.sprintf "[%u]" x)
+ | D.Abst (n, x) when N.is_infinite n -> pp_terms "[:" "]" out x
+ | D.Abst (n, x) ->
+ pp_terms "[:" (P.sprintf "]^%s" (N.to_string n)) out x
+ | D.Abbr x -> pp_terms "[=" "]" out x
+ | D.Void x -> out (P.sprintf "[%u]" x)