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

Fix bug in level.cpp. Add new example

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-08-18 18:37:47 -07:00
parent 95cfac426d
commit a46bf357b0
3 changed files with 22 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
examples/ex7.lean Normal file
View file

@ -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

2
src/kernel/level.cpp
View file

@ -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 {

1
src/shell/CMakeLists.txt
View file

@ -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")