From a2c1372d451267aafdd79adaa1972cbc50b60ed4 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 31 May 2016 19:12:02 -0700
Subject: [PATCH] feat(frontends/lean/builtin_cmds): generate better error
 message when vm_eval result is a function

---
 src/frontends/lean/builtin_cmds.cpp | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
index 9c8013e301..fd05308258 100644
--- a/src/frontends/lean/builtin_cmds.cpp
+++ b/src/frontends/lean/builtin_cmds.cpp
@@ -667,9 +667,11 @@ static environment compile_cmd(parser & p) {
 
 static void vm_eval_core(bool is_IO, vm_state & s, name const & main) {
     if (is_IO) s.push(mk_vm_simple(0)); // push the "RealWorld" state
+    vm_decl d = *s.get_decl(main);
+    if (!is_IO && d.get_arity() > 0)
+        throw exception("vm_eval result is a function");
     s.invoke_fn(main);
     if (is_IO) {
-        vm_decl d = *s.get_decl(main);
         if (d.get_arity() == 0) {
             /* main returned a closure, it did not process RealWorld yet.
                So, we force the execution. */