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

fix: remove old assertions

Browse source
This commit is contained in:
Leonardo de Moura 2020-07-08 12:45:53 -07:00
parent 707ca63f87
commit a488ec903e
1 changed files with 0 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/app_builder.cpp
View file

@ -105,7 +105,6 @@ class app_builder {
}
optional<entry> get_entry(name const & c, unsigned nargs) {
lean_assert(k.check_invariant());
if (optional<constant_info> info = env().find(c)) {
buffer<expr> mvars;
buffer<optional<expr>> inst_args;
@ -150,7 +149,6 @@ class app_builder {
}
optional<entry> get_entry(name const & c, unsigned mask_sz, bool const * mask) {
lean_assert(k.check_invariant());
if (auto d = env().find(c)) {
buffer<expr> mvars;
buffer<optional<expr>> inst_args;