Move numerics and sexpr to util
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
parent
1f7011353b
commit
c2ebe42ca8
23 changed files with 9 additions and 9 deletions
|
@ -42,16 +42,16 @@ else()
|
|||
endif()
|
||||
|
||||
include_directories(${LEAN_SOURCE_DIR}/util)
|
||||
include_directories(${LEAN_SOURCE_DIR}/numerics)
|
||||
include_directories(${LEAN_SOURCE_DIR}/util/numerics)
|
||||
include_directories(${LEAN_SOURCE_DIR}/util/sexpr)
|
||||
include_directories(${LEAN_SOURCE_DIR}/interval)
|
||||
include_directories(${LEAN_SOURCE_DIR}/sexpr)
|
||||
include_directories(${LEAN_SOURCE_DIR}/kernel)
|
||||
|
||||
add_subdirectory(util)
|
||||
set(EXTRA_LIBS ${EXTRA_LIBS} util)
|
||||
add_subdirectory(numerics)
|
||||
add_subdirectory(util/numerics)
|
||||
set(EXTRA_LIBS ${EXTRA_LIBS} numerics)
|
||||
add_subdirectory(sexpr)
|
||||
add_subdirectory(util/sexpr)
|
||||
set(EXTRA_LIBS ${EXTRA_LIBS} sexpr)
|
||||
add_subdirectory(interval)
|
||||
set(EXTRA_LIBS ${EXTRA_LIBS} interval)
|
||||
|
@ -60,7 +60,7 @@ set(EXTRA_LIBS ${EXTRA_LIBS} kernel)
|
|||
set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -pthread")
|
||||
add_subdirectory(shell)
|
||||
add_subdirectory(tests/util)
|
||||
add_subdirectory(tests/numerics)
|
||||
add_subdirectory(tests/util/numerics)
|
||||
add_subdirectory(tests/util/sexpr)
|
||||
add_subdirectory(tests/interval)
|
||||
add_subdirectory(tests/sexpr)
|
||||
add_subdirectory(tests/kernel)
|
||||
|
|
|
@ -109,9 +109,9 @@ unsigned depth3(expr const & e) {
|
|||
void tst2() {
|
||||
expr r1 = mk_dag(20);
|
||||
expr r2 = mk_dag(20);
|
||||
lean_verify(r1 == r2);
|
||||
lean_assert(r1 == r2);
|
||||
std::cout << depth2(r1) << "\n";
|
||||
lean_verify(depth2(r1) == 21);
|
||||
lean_assert(depth2(r1) == 21);
|
||||
}
|
||||
|
||||
expr mk_big(expr f, unsigned depth, unsigned val) {
|
||||
|
@ -125,7 +125,7 @@ void tst3() {
|
|||
expr f = constant("f");
|
||||
expr r1 = mk_big(f, 18, 0);
|
||||
expr r2 = mk_big(f, 18, 0);
|
||||
lean_verify(r1 == r2);
|
||||
lean_assert(r1 == r2);
|
||||
}
|
||||
|
||||
void tst4() {
|
||||
|
|
Loading…
Reference in a new issue