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

chore(*): fix compilation warnings

Browse source
This commit is contained in:
Leonardo de Moura 2016-09-19 17:36:28 -07:00
parent e98340ddae
commit 165e2d5b97
4 changed files with 4 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/frontends/lean/inductive_cmds.cpp
View file

@ -71,7 +71,6 @@ class inductive_cmd_fn {
level m_u; // temporary auxiliary global universe used for inferring the result
// universe of an inductive datatype declaration.
bool m_infer_result_universe{false};
bool m_found_nested_universe{false};
[[ noreturn ]] void throw_error(char const * error_msg) const { throw parser_error(error_msg, m_pos); }
[[ noreturn ]] void throw_error(sstream const & strm) const { throw parser_error(strm, m_pos); }

4
src/library/inductive_compiler/util.cpp
View file

@ -49,8 +49,8 @@ void assert_no_locals(name const & n, expr const & e) {
lean_assert(false);
}
void assert_def_eq(environment const & env, expr const & e1, expr const & e2) {
type_checker checker(env);
void assert_def_eq(environment const & DEBUG_CODE(env), expr const & DEBUG_CODE(e1), expr const & DEBUG_CODE(e2)) {
DEBUG_CODE(type_checker checker(env););
try {
lean_assert(checker.is_def_eq(e1, e2));
} catch (exception ex) {

2
src/library/reducible.cpp
View file

@ -49,7 +49,7 @@ public:
reducibility_proxy_attribute(char const * id, char const * descr, reducible_status m_status):
parent(id, descr, m_status) {}
virtual typed_attribute<reducibility_attribute_data> const & get_attribute() const {
virtual typed_attribute<reducibility_attribute_data> const & get_attribute() const override {
return get_reducibility_attribute();
}

2
src/util/subscripted_name_set.cpp
View file

@ -13,7 +13,7 @@ void subscripted_name_set::check_invariants() const {
if (auto is_subscripted = n.is_subscripted()) {
auto subscripts = m_prefixes.find(is_subscripted->first);
lean_assert(subscripts);
auto free_region = subscripts->find_next_greater_or_equal(closed_ival(is_subscripted->second));
DEBUG_CODE(auto free_region =) subscripts->find_next_greater_or_equal(closed_ival(is_subscripted->second));
lean_assert(free_region);
lean_assert(!free_region->contains(is_subscripted->second));
}