From 67de3b06f3304a3f4a82f2c16f58fc553ee35735 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 14 Nov 2014 14:51:03 -0800 Subject: [PATCH] feat(kernel/level): improve universe level pretty printer Example: produce `l+2` instead of `succ (succ l)`. --- src/kernel/level.cpp | 6 ++++-- tests/lean/prodtst.lean.expected.out | 2 +- tests/lean/univ_vars.lean.expected.out | 2 +- 3 files changed, 6 insertions(+), 4 deletions(-) diff --git a/src/kernel/level.cpp b/src/kernel/level.cpp index 645e26f17..5bf46ec4e 100644 --- a/src/kernel/level.cpp +++ b/src/kernel/level.cpp @@ -517,8 +517,10 @@ format pp(level l, bool unicode, unsigned indent) { return format(to_param_core(l).m_id); case level_kind::Meta: return format("?") + format(meta_id(l)); - case level_kind::Succ: - return group(compose(format("succ"), nest(indent, compose(line(), pp_child(succ_of(l), unicode, indent))))); + case level_kind::Succ: { + auto p = to_offset(l); + return format{pp_child(p.first, unicode, indent), format("+"), format(p.second)}; + } case level_kind::Max: case level_kind::IMax: { format r = format(is_max(l) ? "max" : "imax"); r += nest(indent, compose(line(), pp_child(to_max_core(l).m_lhs, unicode, indent))); diff --git a/tests/lean/prodtst.lean.expected.out b/tests/lean/prodtst.lean.expected.out index f563850f2..c5091d6e8 100644 --- a/tests/lean/prodtst.lean.expected.out +++ b/tests/lean/prodtst.lean.expected.out @@ -1 +1 @@ -prod.{l_1 l_2} : Type.{succ l_1} → Type.{succ l_2} → Type.{max (succ l_1) (succ l_2)} +prod.{l_1 l_2} : Type.{l_1+1} → Type.{l_2+1} → Type.{max (l_1+1) (l_2+1)} diff --git a/tests/lean/univ_vars.lean.expected.out b/tests/lean/univ_vars.lean.expected.out index cdf612f48..9c12fc386 100644 --- a/tests/lean/univ_vars.lean.expected.out +++ b/tests/lean/univ_vars.lean.expected.out @@ -2,4 +2,4 @@ id1 : Π (A : Type.{u}), A → A id2.{l_2} : Π (B : Type.{l_2}), B → B id3.{l_2} : Π (C : Type.{l_2}), C → C foo.{l_2} : Π (A₁ A₂ : Type.{l_2}), A₁ → A₂ → Prop -Type.{m} : Type.{succ m} +Type.{m} : Type.{m+1}