From a46bf357b01068cfccd2e2bfe27205ff4bbde025 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 18 Aug 2013 18:37:47 -0700
Subject: [PATCH] Fix bug in level.cpp. Add new example

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 examples/ex7.lean        | 20 ++++++++++++++++++++
 src/kernel/level.cpp     |  2 +-
 src/shell/CMakeLists.txt |  1 +
 3 files changed, 22 insertions(+), 1 deletion(-)
 create mode 100644 examples/ex7.lean

diff --git a/examples/ex7.lean b/examples/ex7.lean
new file mode 100644
index 000000000..9a176f435
--- /dev/null
+++ b/examples/ex7.lean
@@ -0,0 +1,20 @@
+Variable x : Type max u+1+2 m+1 m+2 3
+Check x
+Variable f : Type u+10 -> Type
+Check f
+Check f x
+Check Type 4
+Check x
+Check Type max u m
+Show Type u+3
+Check Type u+3
+Check Type u ⊓ m
+Check Type u ⊓ m ⊓ 3
+Show Type u+1 ⊓ m ⊓ 3
+Check Type u+1 ⊓ m ⊓ 3
+Show Type u -> Type 5
+Check Type u -> Type 5
+Check Type m ⊓ 3 -> Type u+5
+Show Type m ⊓ 3 -> Type u -> Type 5
+Check Type m ⊓ 3 -> Type u -> Type 5
+Show Type u
diff --git a/src/kernel/level.cpp b/src/kernel/level.cpp
index 7335f22cd..edabd90c9 100644
--- a/src/kernel/level.cpp
+++ b/src/kernel/level.cpp
@@ -127,7 +127,7 @@ level max_core(level_max * l1, level_max * l2) { return max_core(l1->m_size, l1-
 level max(level const & l1, level const & l2) {
     if (is_max(l1)) {
         if (is_max(l2))
-            return max_core(to_max(l1), to_max(l1));
+            return max_core(to_max(l1), to_max(l2));
         else
             return max_core(to_max(l1), l2);
     } else {
diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt
index d0b8e6d4e..866043d11 100644
--- a/src/shell/CMakeLists.txt
+++ b/src/shell/CMakeLists.txt
@@ -8,3 +8,4 @@ add_test(lean3 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../examples/
 add_test(lean4 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../examples/ex4.lean")
 add_test(lean5 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../examples/ex5.lean")
 add_test(lean6 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../examples/ex6.lean")
+add_test(lean7 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../examples/ex7.lean")