From d5184a1751c3f8d154c68ab9465acd728bcebb0f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 14 May 2014 16:51:49 -0700 Subject: [PATCH] feat(kernel/formatter): print binder_info in simple formater Signed-off-by: Leonardo de Moura --- src/kernel/formatter.cpp | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/src/kernel/formatter.cpp b/src/kernel/formatter.cpp index e29469f67..51b3c8355 100644 --- a/src/kernel/formatter.cpp +++ b/src/kernel/formatter.cpp @@ -66,8 +66,17 @@ struct print_expr_fn { } void print_binder(char const * bname, expr const & e, context const & c) { - out() << bname << " " << binder_name(e) << " : "; + out() << bname << " "; + if (binder_info(e).is_implicit()) + out() << "{"; + else if (binder_info(e).is_cast()) + out() << "["; + out() << binder_name(e) << " : "; print_child(binder_domain(e), c); + if (binder_info(e).is_implicit()) + out() << "}"; + else if (binder_info(e).is_cast()) + out() << "]"; out() << ", "; print_child(binder_body(e), extend(c, binder_name(e), binder_domain(e))); }