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

fix(frontends/lean/pp): fix how Type expressions are pretty printed

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-10-05 15:31:24 -07:00
parent a5c3829d1b
commit f0e149d77b
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/frontends/lean/pp.cpp
View file

@ -198,8 +198,10 @@ class pp_fn {
*/
bool is_atomic(expr const & e) {
switch (e.kind()) {
case expr_kind::Var: case expr_kind::Constant: case expr_kind::Value: case expr_kind::Type:
case expr_kind::Var: case expr_kind::Constant: case expr_kind::Value:
return true;
case expr_kind::Type:
return e == Type();
case expr_kind::MetaVar:
return !metavar_lctx(e);
case expr_kind::App: