max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(util/sexpr/format): preparing to switch to Lean implementation

Browse source
This commit is contained in:
Leonardo de Moura 2019-06-07 10:18:23 -07:00
parent 452485a706
commit 5eaca0d89e
1 changed files with 1 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/util/sexpr/format.h
View file

@ -152,16 +152,12 @@ public:
return sexpr_kind(m_value);
}
bool is_nil_fmt() const { return kind() == format_kind::NIL; }
unsigned hash() const { return m_value.hash(); }
friend format compose(format const & f1, format const & f2);
friend format nest(int i, format const & f);
friend format mk_line();
friend format group(format const & f);
friend format above(format const & f1, format const & f2);
friend format bracket(std::string const & l, format const & x, std::string const & r);
friend format wrap(format const & f1, format const & f2);
friend format flatten(format const & f);
// x + y = x <> y
@ -171,13 +167,6 @@ public:
return *this;
}
// x ^ y = x <> " " <> y
friend format operator^(format const & f1, format const & f2);
format & operator^=(format const & f) {
*this = *this ^ f;
return *this;
}
static std::ostream & pretty(std::ostream & out, unsigned w, format const & f);
friend std::ostream & pretty(std::ostream & out, unsigned w, format const & f);
friend std::ostream & pretty(std::ostream & out, options const & o, format const & f);
@ -186,13 +175,12 @@ public:
friend std::ostream & operator<<(std::ostream & out, pair<format const &, options const &> const & p);
};
format wrap(format const & f1, format const & f2);
format compose(format const & f1, format const & f2);
format nest(int i, format const & f);
format line();
format space();
format group(format const & f);
format bracket(std::string const & l, format const & x, std::string const & r);
format group(format const & f);
format paren(format const & x);
class options;