michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(kernel/level): improve universe level pretty printer

Browse source 
Example: produce `l+2` instead of `succ (succ l)`.
This commit is contained in:
Leonardo de Moura 2014-11-14 14:51:03 -08:00
parent 00df34a1c4
commit 67de3b06f3
3 changed files with 6 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/kernel/level.cpp
View file

@ -517,8 +517,10 @@ format pp(level l, bool unicode, unsigned indent) {
return format(to_param_core(l).m_id); return format(to_param_core(l).m_id);
case level_kind::Meta: case level_kind::Meta:
return format("?") + format(meta_id(l)); return format("?") + format(meta_id(l));
case level_kind::Succ: case level_kind::Succ: {
return group(compose(format("succ"), nest(indent, compose(line(), pp_child(succ_of(l), unicode, indent))))); 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: { case level_kind::Max: case level_kind::IMax: {
format r = format(is_max(l) ? "max" : "imax"); format r = format(is_max(l) ? "max" : "imax");
r += nest(indent, compose(line(), pp_child(to_max_core(l).m_lhs, unicode, indent))); r += nest(indent, compose(line(), pp_child(to_max_core(l).m_lhs, unicode, indent)));

2
tests/lean/prodtst.lean.expected.out
View file

@ -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)}

2
tests/lean/univ_vars.lean.expected.out
View file

@ -2,4 +2,4 @@ id1 : Π (A : Type.{u}), A → A
id2.{l_2} : Π (B : Type.{l_2}), B → B id2.{l_2} : Π (B : Type.{l_2}), B → B
id3.{l_2} : Π (C : Type.{l_2}), C → C id3.{l_2} : Π (C : Type.{l_2}), C → C
foo.{l_2} : Π (A₁ A₂ : Type.{l_2}), A₁ → A₂ → Prop foo.{l_2} : Π (A₁ A₂ : Type.{l_2}), A₁ → A₂ → Prop
Type.{m} : Type.{succ m} Type.{m} : Type.{m+1}