max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(checker/simple_pp): pretty-print changed Sort/Prop/Type

Browse source
This commit is contained in:
Gabriel Ebner 2017-01-31 10:20:06 +01:00
parent bc75c2423f
commit fb9b719a22
1 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/checker/simple_pp.cpp
View file

@ -97,8 +97,10 @@ struct simple_pp_fn {
return format("Prop");
} else if (sort_level(e) == mk_level_one()) {
return format("Type");
} else if (is_succ(sort_level(e))) {
return compose_many({format("Type"), space(), pp_level(succ_of(sort_level(e))).maybe_paren()});
} else {
return compose_many({format("Type"), space(), pp_level(sort_level(e)).maybe_paren()});
return compose_many({format("Sort"), space(), pp_level(sort_level(e)).maybe_paren()});
}
}