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

feat(kernel/instantiate): relax apply_beta pre-conditions

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-05-25 06:57:13 -07:00
parent 1ee6bb48fc
commit f050308df7
1 changed files with 3 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/kernel/instantiate.cpp
View file

@ -56,8 +56,9 @@ bool is_head_beta(expr const & t) {
} }
expr apply_beta(expr f, unsigned num_args, expr const * args) { expr apply_beta(expr f, unsigned num_args, expr const * args) {
lean_assert(num_args > 0); if (num_args == 0) {
if (!is_lambda(f)) { return f;
} else if (!is_lambda(f)) {
return mk_rev_app(f, num_args, args); return mk_rev_app(f, num_args, args);
} else { } else {
unsigned m = 1; unsigned m = 1;