Rename pp functions (that do not use format lib) to print
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
parent
dd21cdcc95
commit
84de625ee4
9 changed files with 12 additions and 9 deletions
|
@ -13,5 +13,5 @@ template class interval<mpq>;
|
|||
template class interval<double>;
|
||||
}
|
||||
|
||||
void pp(lean::interval<lean::mpq> const & i) { std::cout << i << std::endl; }
|
||||
void pp(lean::interval<double> const & i) { std::cout << i << std::endl; }
|
||||
void print(lean::interval<lean::mpq> const & i) { std::cout << i << std::endl; }
|
||||
void print(lean::interval<double> const & i) { std::cout << i << std::endl; }
|
||||
|
|
|
@ -297,7 +297,9 @@ lean::format pp_aux(lean::expr const & a) {
|
|||
return format();
|
||||
}
|
||||
|
||||
void print(lean::expr const & a) { std::cout << a << "\n"; }
|
||||
|
||||
void pp(lean::expr const & a) {
|
||||
lean::format const & f = pp_aux(a);
|
||||
std::cout << f;
|
||||
std::cout << f << "\n";
|
||||
}
|
||||
|
|
|
@ -472,3 +472,4 @@ template<typename F> expr update_eq(expr const & e, F f) {
|
|||
// =======================================
|
||||
}
|
||||
void pp(lean::expr const & a);
|
||||
void print(lean::expr const & a);
|
||||
|
|
|
@ -263,4 +263,4 @@ std::ostream & operator<<(std::ostream & out, name::sep const & s) {
|
|||
}
|
||||
}
|
||||
|
||||
void pp(lean::name const & n) { std::cout << n << std::endl; }
|
||||
void print(lean::name const & n) { std::cout << n << std::endl; }
|
||||
|
|
|
@ -350,4 +350,4 @@ void display_decimal(std::ostream & out, mpbq const & a, unsigned prec) {
|
|||
|
||||
}
|
||||
|
||||
void pp(lean::mpbq const & n) { std::cout << n << std::endl; }
|
||||
void print(lean::mpbq const & n) { std::cout << n << std::endl; }
|
||||
|
|
|
@ -118,4 +118,4 @@ std::ostream & operator<<(std::ostream & out, mpfp const & v) {
|
|||
|
||||
}
|
||||
|
||||
// void pp(lean::mpq const & v) { std::cout << v << std::endl; }
|
||||
// void print(lean::mpq const & v) { std::cout << v << std::endl; }
|
||||
|
|
|
@ -113,4 +113,4 @@ void display_decimal(std::ostream & out, mpq const & a, unsigned prec) {
|
|||
}
|
||||
}
|
||||
|
||||
void pp(lean::mpq const & v) { std::cout << v << std::endl; }
|
||||
void print(lean::mpq const & v) { std::cout << v << std::endl; }
|
||||
|
|
|
@ -77,4 +77,4 @@ std::ostream & operator<<(std::ostream & out, mpz const & v) {
|
|||
|
||||
}
|
||||
|
||||
void pp(lean::mpz const & n) { std::cout << n << std::endl; }
|
||||
void print(lean::mpz const & n) { std::cout << n << std::endl; }
|
||||
|
|
|
@ -246,4 +246,4 @@ bool operator==(sexpr const & a, mpq const & b) { return is_mpq(a) && to_mpq(a)
|
|||
|
||||
}
|
||||
|
||||
void pp(lean::sexpr const & n) { std::cout << n << "\n"; }
|
||||
void print(lean::sexpr const & n) { std::cout << n << "\n"; }
|
||||
|
|
Loading…
Reference in a new issue