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

perf(library/metavar_util): do nothing if term does not contain assigned metavars

Browse source
This commit is contained in:
Leonardo de Moura 2016-06-20 09:06:04 -07:00
parent 02904c5b87
commit a2745aa273
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/metavar_util.h
View file

@ -194,6 +194,8 @@ public:
template<typename CTX>
expr instantiate_mvars(CTX & ctx, expr const & e) {
if (!has_assigned(ctx, e))
return e;
return instantiate_mvars_fn<CTX>(ctx)(e);
}
}