From 1fb526a3d495194ac77ab27ebdbec8e164f765a0 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 10 Dec 2013 16:18:45 -0800
Subject: [PATCH] perf(library/type_inferer): improve is_proposition
 performance

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/library/type_inferer.cpp | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/src/library/type_inferer.cpp b/src/library/type_inferer.cpp
index b0677d139..2ff9be6f2 100644
--- a/src/library/type_inferer.cpp
+++ b/src/library/type_inferer.cpp
@@ -240,6 +240,12 @@ public:
     }
 
     bool is_proposition(expr const & e, context const & ctx, metavar_env * menv) {
+        // Catch easy cases
+        switch (e.kind()) {
+        case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Type: return false;
+        case expr_kind::Eq: return true;
+        default: break;
+        }
         expr t = operator()(e, ctx, menv, nullptr);
         if (is_bool(t))
             return true;