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

Modify basic printer for contexts

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-08-23 12:08:49 -07:00
parent 18a195029b
commit e95a0c2559
1 changed files with 10 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/library/printer.cpp
View file

@ -139,15 +139,22 @@ std::ostream & operator<<(std::ostream & out, std::pair<expr const &, context co
return out;
}
std::ostream & operator<<(std::ostream & out, context const & ctx) {
static void display_context_core(std::ostream & out, context const & ctx) {
if (ctx) {
out << tail(ctx);
display_context_core(out, tail(ctx));
if (tail(ctx))
out << "; ";
out << head(ctx).get_name() << " : " << head(ctx).get_domain();
if (head(ctx).get_body()) {
out << " := " << mk_pair(head(ctx).get_body(), tail(ctx));
}
out << "\n";
}
}
std::ostream & operator<<(std::ostream & out, context const & ctx) {
out << "[";
display_context_core(out, ctx);
out << "]";
return out;
}