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

fix(library/idx_metavar): compilation problem in debug mode

Browse source
This commit is contained in:
Leonardo de Moura 2015-06-09 14:37:17 -07:00
parent e3a0e62859
commit f3d50963ce
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/library/idx_metavar.cpp
View file

@ -38,7 +38,7 @@ bool is_idx_metauniv(level const & l) {
}
unsigned to_meta_idx(level const & l) {
lean_assert(is_idx_meta_univ(l));
lean_assert(is_idx_metauniv(l));
return meta_id(l).get_numeral();
}
@ -50,7 +50,7 @@ bool is_idx_metavar(expr const & e) {
}
unsigned to_meta_idx(expr const & e) {
lean_assert(is_idx_meta(e));
lean_assert(is_idx_metavar(e));
return mlocal_name(e).get_numeral();
}
}