From fb9b719a222998d72fe03b32afd286db37db1a17 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Tue, 31 Jan 2017 10:20:06 +0100 Subject: [PATCH] chore(checker/simple_pp): pretty-print changed Sort/Prop/Type --- src/checker/simple_pp.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/checker/simple_pp.cpp b/src/checker/simple_pp.cpp index 3be157f2c5..15d285bcc7 100644 --- a/src/checker/simple_pp.cpp +++ b/src/checker/simple_pp.cpp @@ -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()}); } }