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

chore(library/local_context): style

Browse source
This commit is contained in:
Leonardo de Moura 2017-01-03 15:00:46 -08:00
parent 554cef1d36
commit d546671849
2 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/local_context.cpp
View file

@ -337,7 +337,7 @@ bool local_context::well_formed(expr const & e) const {
return ok;
}
format local_context::pp(formatter const & fmt, std::function<bool(local_decl const &)> const & pred) const {
format local_context::pp(formatter const & fmt, std::function<bool(local_decl const &)> const & pred) const { // NOLINT
options const & opts = fmt.get_options();
unsigned indent = get_pp_indent(opts);
unsigned max_hs = get_pp_goal_max_hyps(opts);

2
src/library/local_context.h
View file

@ -177,7 +177,7 @@ public:
That is, all local_decl references in \c e are defined in this context. */
bool well_formed(expr const & e) const;
format pp(formatter const & fmt, std::function<bool(local_decl const &)> const & pred) const;
format pp(formatter const & fmt, std::function<bool(local_decl const &)> const & pred) const; // NOLINT
format pp(formatter const & fmt) const { return pp(fmt, [](local_decl const &) { return true; }); }
/** \brief Replaced assigned metavariables with their values.