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

fix(kernel/metavar): compilation error in some compilers

Browse source
This commit is contained in:
Leonardo de Moura 2014-10-17 17:22:25 -07:00
parent 6285c3a217
commit 1ce3b83d79
2 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/kernel/metavar.cpp
View file

@ -337,7 +337,7 @@ name_set substitution::get_occs(name const & m, name_set & fresh) {
} }
} }
bool substitution::occurs_expr(name const & m, expr const & e) const { bool substitution::occurs_expr(name const & m, expr const & e) {
if (!has_expr_metavar(e)) if (!has_expr_metavar(e))
return false; return false;
name_set fresh; name_set fresh;

4
src/kernel/metavar.h
View file

@ -105,7 +105,7 @@ public:
optional<level> get_level(level const & m) const { lean_assert(is_meta(m)); return get_level(meta_id(m)); } optional<level> get_level(level const & m) const { lean_assert(is_meta(m)); return get_level(meta_id(m)); }
/** \brief Return true iff the metavariable \c m occurrs (directly or indirectly) in \c e. */ /** \brief Return true iff the metavariable \c m occurrs (directly or indirectly) in \c e. */
bool occurs_expr(name const & m, expr const & e) const; bool occurs_expr(name const & m, expr const & e);
bool occurs(expr const & m, expr const & e) const { lean_assert(is_metavar(m)); return occurs_expr(mlocal_name(m), e); } bool occurs(expr const & m, expr const & e) { lean_assert(is_metavar(m)); return occurs_expr(mlocal_name(m), e); }
}; };
} }