From f050308df72def952e62483e3eadd3ad62632669 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 25 May 2014 06:57:13 -0700
Subject: [PATCH] feat(kernel/instantiate): relax apply_beta pre-conditions

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/kernel/instantiate.cpp | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/kernel/instantiate.cpp b/src/kernel/instantiate.cpp
index e6701ff94..4484ba93b 100644
--- a/src/kernel/instantiate.cpp
+++ b/src/kernel/instantiate.cpp
@@ -56,8 +56,9 @@ bool is_head_beta(expr const & t) {
 }
 
 expr apply_beta(expr f, unsigned num_args, expr const * args) {
-    lean_assert(num_args > 0);
-    if (!is_lambda(f)) {
+    if (num_args == 0) {
+        return f;
+    } else if (!is_lambda(f)) {
         return mk_rev_app(f, num_args, args);
     } else {
         unsigned m = 1;