diff options
Diffstat (limited to 'math/lean4')
| -rw-r--r-- | math/lean4/Makefile | 13 | ||||
| -rw-r--r-- | math/lean4/distinfo | 6 | ||||
| -rw-r--r-- | math/lean4/files/patch-src_CMakeLists.txt | 13 | ||||
| -rw-r--r-- | math/lean4/files/patch-src_bin_leanc.in | 11 | ||||
| -rw-r--r-- | math/lean4/files/patch-src_runtime_io.cpp | 4 | ||||
| -rw-r--r-- | math/lean4/files/patch-src_runtime_process.cpp | 22 | ||||
| -rw-r--r-- | math/lean4/files/patch-src_runtime_stack__overflow.cpp | 6 | ||||
| -rw-r--r-- | math/lean4/files/patch-stage0_src_CMakeLists.txt | 13 | ||||
| -rw-r--r-- | math/lean4/files/patch-stage0_src_bin_leanc.in | 11 | ||||
| -rw-r--r-- | math/lean4/files/patch-stage0_src_runtime_io.cpp | 4 | ||||
| -rw-r--r-- | math/lean4/files/patch-stage0_src_runtime_process.cpp | 22 | ||||
| -rw-r--r-- | math/lean4/files/patch-stage0_src_runtime_stack__overflow.cpp | 6 | ||||
| -rw-r--r-- | math/lean4/pkg-plist | 2025 |
13 files changed, 2016 insertions, 140 deletions
diff --git a/math/lean4/Makefile b/math/lean4/Makefile index 3e7cfb67dfd9..56155b9be891 100644 --- a/math/lean4/Makefile +++ b/math/lean4/Makefile @@ -1,11 +1,12 @@ PORTNAME= lean4 DISTVERSIONPREFIX= v -DISTVERSION= 4.12.0 +DISTVERSION= 4.20.0-rc5 CATEGORIES= math lang devel # lean4 is primarily a math theorem prover, but it is also a language and a development environment MAINTAINER= yuri@FreeBSD.org COMMENT= Theorem prover and functional language for math (new gen) -WWW= https://lean-lang.org/ +WWW= https://lean-lang.org/ \ + https://github.com/leanprover/lean4 LICENSE= APACHE20 LICENSE_FILE= ${WRKSRC}/LICENSE @@ -19,7 +20,7 @@ LIB_DEPENDS= libgmp.so:math/gmp \ libuv.so:devel/libuv RUN_DEPENDS= cadical:math/cadical -USES= cmake:noninja,testing compiler:c++14-lang gmake python:build # ninja fails + gmake scripts are included in the project +USES= cmake:noninja,testing compiler:c++14-lang gmake pkgconfig python:build # ninja fails + gmake scripts are included in the project USE_GITHUB= yes GH_ACCOUNT= leanprover @@ -27,6 +28,12 @@ GH_ACCOUNT= leanprover CFLAGS+= -fPIC CXXFLAGS+= -fPIC +CMAKE_OFF= USE_MIMALLOC + +#MAKE_ARGS+= V=1 VERBOSE=1 +#MAKE_JOBS_UNSAFE= yes +MAKE_ENV= LD_LIBRARY_PATH=${BUILD_WRKSRC}/stage0/lib/lean + BINARY_ALIAS= make=${GMAKE} python=${PYTHON_CMD} pre-everything:: diff --git a/math/lean4/distinfo b/math/lean4/distinfo index d2357b8b5f44..5aef4f3763ae 100644 --- a/math/lean4/distinfo +++ b/math/lean4/distinfo @@ -1,3 +1,3 @@ -TIMESTAMP = 1727897287 -SHA256 (leanprover-lean4-v4.12.0_GH0.tar.gz) = 409f623eb9044b3b025951415dfa0db531ed29056a5fba5d556394ad9435e62b -SIZE (leanprover-lean4-v4.12.0_GH0.tar.gz) = 27334919 +TIMESTAMP = 1746632807 +SHA256 (leanprover-lean4-v4.20.0-rc5_GH0.tar.gz) = aaddadf237e16bdb2fd06987315f4af0791dfa965a924511087865d441b80ec6 +SIZE (leanprover-lean4-v4.20.0-rc5_GH0.tar.gz) = 40328367 diff --git a/math/lean4/files/patch-src_CMakeLists.txt b/math/lean4/files/patch-src_CMakeLists.txt index 98298fd62d75..d7658e68a521 100644 --- a/math/lean4/files/patch-src_CMakeLists.txt +++ b/math/lean4/files/patch-src_CMakeLists.txt @@ -1,9 +1,9 @@ ---- src/CMakeLists.txt.orig 2024-03-06 02:11:32 UTC +--- src/CMakeLists.txt.orig 2025-05-07 10:26:21 UTC +++ src/CMakeLists.txt -@@ -362,6 +362,15 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Linux") - string(APPEND LEANC_EXTRA_FLAGS " -fPIC") +@@ -472,6 +472,16 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Linux") string(APPEND TOOLCHAIN_SHARED_LINKER_FLAGS " -Wl,-rpath=\\$$ORIGIN/..:\\$$ORIGIN") - string(APPEND CMAKE_EXE_LINKER_FLAGS " -Wl,-rpath=\\\$ORIGIN/../lib:\\\$ORIGIN/../lib/lean") + string(APPEND LAKESHARED_LINKER_FLAGS " -Wl,--whole-archive ${CMAKE_BINARY_DIR}/lib/lean/libLake.a.export -Wl,--no-whole-archive") + string(APPEND CMAKE_EXE_LINKER_FLAGS " -Wl,-rpath=$ORIGIN/../lib:$ORIGIN/../lib/lean") +elseif(${CMAKE_SYSTEM_NAME} MATCHES "FreeBSD") + if(BSYMBOLIC) + string(APPEND LEANC_SHARED_LINKER_FLAGS " -Wl,-Bsymbolic") @@ -12,11 +12,12 @@ + string(APPEND CMAKE_CXX_FLAGS " -fPIC -ftls-model=initial-exec") + string(APPEND LEANC_EXTRA_FLAGS " -fPIC") + string(APPEND TOOLCHAIN_SHARED_LINKER_FLAGS " -Wl,-rpath=\\$$ORIGIN/..:\\$$ORIGIN") -+ string(APPEND CMAKE_EXE_LINKER_FLAGS " -Wl,-rpath=\\\$ORIGIN/../lib:\\\$ORIGIN/../lib/lean") ++ string(APPEND LAKESHARED_LINKER_FLAGS " -Wl,--whole-archive ${CMAKE_BINARY_DIR}/lib/lean/libLake.a.export -Wl,--no-whole-archive") ++ string(APPEND CMAKE_EXE_LINKER_FLAGS " -Wl,-rpath=$ORIGIN/../lib:$ORIGIN/../lib/lean") elseif(${CMAKE_SYSTEM_NAME} MATCHES "Darwin") string(APPEND CMAKE_CXX_FLAGS " -ftls-model=initial-exec") string(APPEND INIT_SHARED_LINKER_FLAGS " -install_name @rpath/libInit_shared.dylib") -@@ -624,7 +633,7 @@ endif() +@@ -801,7 +811,7 @@ endif() file(CREATE_LINK ${CMAKE_SOURCE_DIR} ${CMAKE_BINARY_DIR}/src/lean RESULT _IGNORE_RES SYMBOLIC) endif() diff --git a/math/lean4/files/patch-src_bin_leanc.in b/math/lean4/files/patch-src_bin_leanc.in new file mode 100644 index 000000000000..6b110ae220b3 --- /dev/null +++ b/math/lean4/files/patch-src_bin_leanc.in @@ -0,0 +1,11 @@ +--- src/bin/leanc.in.orig 2025-05-07 10:26:21 UTC ++++ src/bin/leanc.in +@@ -7,7 +7,7 @@ done + [[ "$arg" = "-c" ]] && ldflags=() + [[ "$arg" = "-v" ]] && v=1 + done +-cmd=(${LEAN_CC:-@CMAKE_C_COMPILER@} "-I$root/include" @LEANC_EXTRA_CC_FLAGS@ @LEANC_INTERNAL_FLAGS@ "$@" "${ldflags[@]}" -Wno-unused-command-line-argument) ++cmd=(${LEAN_CC:-@CMAKE_C_COMPILER@} "-I$root/include" @LEANC_EXTRA_CC_FLAGS@ @LEANC_INTERNAL_FLAGS@ "$@" "${ldflags[@]}" -Wno-unused-command-line-argument -fPIC) + cmd=$(printf '%q ' "${cmd[@]}" | sed "s!ROOT!$root!g") + [[ $v == 1 ]] && echo $cmd + eval $cmd diff --git a/math/lean4/files/patch-src_runtime_io.cpp b/math/lean4/files/patch-src_runtime_io.cpp index 767ad0a1625f..2e185dfb816c 100644 --- a/math/lean4/files/patch-src_runtime_io.cpp +++ b/math/lean4/files/patch-src_runtime_io.cpp @@ -1,6 +1,6 @@ ---- src/runtime/io.cpp.orig 2024-01-13 17:13:25 UTC +--- src/runtime/io.cpp.orig 2025-05-06 09:12:17 UTC +++ src/runtime/io.cpp -@@ -855,7 +855,13 @@ extern "C" LEAN_EXPORT obj_res lean_io_app_path(obj_ar +@@ -1253,7 +1253,13 @@ extern "C" LEAN_EXPORT obj_res lean_io_app_path(obj_ar char dest[PATH_MAX]; memset(dest, 0, PATH_MAX); pid_t pid = getpid(); diff --git a/math/lean4/files/patch-src_runtime_process.cpp b/math/lean4/files/patch-src_runtime_process.cpp new file mode 100644 index 000000000000..b13998f4743f --- /dev/null +++ b/math/lean4/files/patch-src_runtime_process.cpp @@ -0,0 +1,22 @@ +--- src/runtime/process.cpp.orig 2025-05-06 09:12:17 UTC ++++ src/runtime/process.cpp +@@ -31,6 +31,10 @@ Author: Jared Roesch + #include <sys/syscall.h> + #endif + ++#ifdef __FreeBSD__ ++#include <pthread_np.h> ++#endif ++ + #include "runtime/object.h" + #include "runtime/io.h" + #include "runtime/array_ref.h" +@@ -342,6 +346,8 @@ extern "C" LEAN_EXPORT obj_res lean_io_get_tid(obj_arg + lean_always_assert(pthread_threadid_np(NULL, &tid) == 0); + #elif defined(LEAN_EMSCRIPTEN) + tid = 0; ++#elif defined(__FreeBSD__) ++ tid = (pid_t)pthread_getthreadid_np(); + #else + // since Linux 2.4.11, our glibc 2.27 requires at least 3.2 + // glibc 2.30 would provide a wrapper diff --git a/math/lean4/files/patch-src_runtime_stack__overflow.cpp b/math/lean4/files/patch-src_runtime_stack__overflow.cpp index 06914304dbaa..cdd63ffde32a 100644 --- a/math/lean4/files/patch-src_runtime_stack__overflow.cpp +++ b/math/lean4/files/patch-src_runtime_stack__overflow.cpp @@ -1,7 +1,7 @@ ---- src/runtime/stack_overflow.cpp.orig 2023-12-21 22:11:33 UTC +--- src/runtime/stack_overflow.cpp.orig 2025-05-06 09:12:17 UTC +++ src/runtime/stack_overflow.cpp -@@ -20,6 +20,9 @@ Port of the corresponding Rust code (see links below). - #include <lean/lean.h> +@@ -21,6 +21,9 @@ Port of the corresponding Rust code (see links below). + #include <initializer_list> #include "runtime/stack_overflow.h" +#include <pthread_np.h> diff --git a/math/lean4/files/patch-stage0_src_CMakeLists.txt b/math/lean4/files/patch-stage0_src_CMakeLists.txt index ec7e8f739ef0..184415ffa3d9 100644 --- a/math/lean4/files/patch-stage0_src_CMakeLists.txt +++ b/math/lean4/files/patch-stage0_src_CMakeLists.txt @@ -1,9 +1,9 @@ ---- stage0/src/CMakeLists.txt.orig 2024-03-06 02:11:32 UTC +--- stage0/src/CMakeLists.txt.orig 2025-05-06 09:12:17 UTC +++ stage0/src/CMakeLists.txt -@@ -362,6 +362,15 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Linux") - string(APPEND LEANC_EXTRA_FLAGS " -fPIC") +@@ -472,6 +472,16 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Linux") string(APPEND TOOLCHAIN_SHARED_LINKER_FLAGS " -Wl,-rpath=\\$$ORIGIN/..:\\$$ORIGIN") - string(APPEND CMAKE_EXE_LINKER_FLAGS " -Wl,-rpath=\\\$ORIGIN/../lib:\\\$ORIGIN/../lib/lean") + string(APPEND LAKESHARED_LINKER_FLAGS " -Wl,--whole-archive ${CMAKE_BINARY_DIR}/lib/lean/libLake.a.export -Wl,--no-whole-archive") + string(APPEND CMAKE_EXE_LINKER_FLAGS " -Wl,-rpath=$ORIGIN/../lib:$ORIGIN/../lib/lean") +elseif(${CMAKE_SYSTEM_NAME} MATCHES "FreeBSD") + if(BSYMBOLIC) + string(APPEND LEANC_SHARED_LINKER_FLAGS " -Wl,-Bsymbolic") @@ -12,11 +12,12 @@ + string(APPEND CMAKE_CXX_FLAGS " -fPIC -ftls-model=initial-exec") + string(APPEND LEANC_EXTRA_FLAGS " -fPIC") + string(APPEND TOOLCHAIN_SHARED_LINKER_FLAGS " -Wl,-rpath=\\$$ORIGIN/..:\\$$ORIGIN") -+ string(APPEND CMAKE_EXE_LINKER_FLAGS " -Wl,-rpath=\\\$ORIGIN/../lib:\\\$ORIGIN/../lib/lean") ++ string(APPEND LAKESHARED_LINKER_FLAGS " -Wl,--whole-archive ${CMAKE_BINARY_DIR}/lib/lean/libLake.a.export -Wl,--no-whole-archive") ++ string(APPEND CMAKE_EXE_LINKER_FLAGS " -Wl,-rpath=$ORIGIN/../lib:$ORIGIN/../lib/lean") elseif(${CMAKE_SYSTEM_NAME} MATCHES "Darwin") string(APPEND CMAKE_CXX_FLAGS " -ftls-model=initial-exec") string(APPEND INIT_SHARED_LINKER_FLAGS " -install_name @rpath/libInit_shared.dylib") -@@ -624,7 +633,7 @@ endif() +@@ -798,7 +808,7 @@ endif() file(CREATE_LINK ${CMAKE_SOURCE_DIR} ${CMAKE_BINARY_DIR}/src/lean RESULT _IGNORE_RES SYMBOLIC) endif() diff --git a/math/lean4/files/patch-stage0_src_bin_leanc.in b/math/lean4/files/patch-stage0_src_bin_leanc.in new file mode 100644 index 000000000000..a6f3f345b929 --- /dev/null +++ b/math/lean4/files/patch-stage0_src_bin_leanc.in @@ -0,0 +1,11 @@ +--- stage0/src/bin/leanc.in.orig 2025-05-07 10:26:21 UTC ++++ stage0/src/bin/leanc.in +@@ -7,7 +7,7 @@ done + [[ "$arg" = "-c" ]] && ldflags=() + [[ "$arg" = "-v" ]] && v=1 + done +-cmd=(${LEAN_CC:-@CMAKE_C_COMPILER@} "-I$root/include" @LEANC_EXTRA_CC_FLAGS@ @LEANC_INTERNAL_FLAGS@ "$@" "${ldflags[@]}" -Wno-unused-command-line-argument) ++cmd=(${LEAN_CC:-@CMAKE_C_COMPILER@} "-I$root/include" @LEANC_EXTRA_CC_FLAGS@ @LEANC_INTERNAL_FLAGS@ "$@" "${ldflags[@]}" -Wno-unused-command-line-argument -fPIC) + cmd=$(printf '%q ' "${cmd[@]}" | sed "s!ROOT!$root!g") + [[ $v == 1 ]] && echo $cmd + eval $cmd diff --git a/math/lean4/files/patch-stage0_src_runtime_io.cpp b/math/lean4/files/patch-stage0_src_runtime_io.cpp index 67d799f2a916..9b00b760a7a8 100644 --- a/math/lean4/files/patch-stage0_src_runtime_io.cpp +++ b/math/lean4/files/patch-stage0_src_runtime_io.cpp @@ -1,6 +1,6 @@ ---- stage0/src/runtime/io.cpp.orig 2024-01-13 09:36:50 UTC +--- stage0/src/runtime/io.cpp.orig 2025-05-06 09:12:17 UTC +++ stage0/src/runtime/io.cpp -@@ -855,7 +855,13 @@ extern "C" LEAN_EXPORT obj_res lean_io_app_path(obj_ar +@@ -1253,7 +1253,13 @@ extern "C" LEAN_EXPORT obj_res lean_io_app_path(obj_ar char dest[PATH_MAX]; memset(dest, 0, PATH_MAX); pid_t pid = getpid(); diff --git a/math/lean4/files/patch-stage0_src_runtime_process.cpp b/math/lean4/files/patch-stage0_src_runtime_process.cpp new file mode 100644 index 000000000000..8b8fb1a9e008 --- /dev/null +++ b/math/lean4/files/patch-stage0_src_runtime_process.cpp @@ -0,0 +1,22 @@ +--- stage0/src/runtime/process.cpp.orig 2025-05-06 09:12:17 UTC ++++ stage0/src/runtime/process.cpp +@@ -31,6 +31,10 @@ Author: Jared Roesch + #include <sys/syscall.h> + #endif + ++#ifdef __FreeBSD__ ++#include <pthread_np.h> ++#endif ++ + #include "runtime/object.h" + #include "runtime/io.h" + #include "runtime/array_ref.h" +@@ -342,6 +346,8 @@ extern "C" LEAN_EXPORT obj_res lean_io_get_tid(obj_arg + lean_always_assert(pthread_threadid_np(NULL, &tid) == 0); + #elif defined(LEAN_EMSCRIPTEN) + tid = 0; ++#elif defined(__FreeBSD__) ++ tid = (pid_t)pthread_getthreadid_np(); + #else + // since Linux 2.4.11, our glibc 2.27 requires at least 3.2 + // glibc 2.30 would provide a wrapper diff --git a/math/lean4/files/patch-stage0_src_runtime_stack__overflow.cpp b/math/lean4/files/patch-stage0_src_runtime_stack__overflow.cpp index 5296c0cf49c2..638daf3af176 100644 --- a/math/lean4/files/patch-stage0_src_runtime_stack__overflow.cpp +++ b/math/lean4/files/patch-stage0_src_runtime_stack__overflow.cpp @@ -1,4 +1,4 @@ ---- stage0/src/runtime/stack_overflow.cpp.orig 2023-12-21 22:11:33 UTC +--- stage0/src/runtime/stack_overflow.cpp.orig 2025-05-06 09:12:17 UTC +++ stage0/src/runtime/stack_overflow.cpp @@ -7,6 +7,10 @@ Port of the corresponding Rust code (see links below). Print a nicer error message on stack overflow. @@ -11,9 +11,9 @@ #ifdef LEAN_WINDOWS #include <windows.h> #else -@@ -19,6 +23,7 @@ Port of the corresponding Rust code (see links below). - #include <cstring> +@@ -20,6 +24,7 @@ Port of the corresponding Rust code (see links below). #include <lean/lean.h> + #include <initializer_list> #include "runtime/stack_overflow.h" + diff --git a/math/lean4/pkg-plist b/math/lean4/pkg-plist index 8093484c1e97..5615db78b1ee 100644 --- a/math/lean4/pkg-plist +++ b/math/lean4/pkg-plist @@ -9,416 +9,1228 @@ include/lean/lean_libuv.h include/lean/version.h lib/lean/Init.ilean lib/lean/Init.olean +lib/lean/Init.olean.private +lib/lean/Init.olean.server +lib/lean/Init/BinderNameHint.ilean +lib/lean/Init/BinderNameHint.olean +lib/lean/Init/BinderNameHint.olean.private +lib/lean/Init/BinderNameHint.olean.server lib/lean/Init/BinderPredicates.ilean lib/lean/Init/BinderPredicates.olean +lib/lean/Init/BinderPredicates.olean.private +lib/lean/Init/BinderPredicates.olean.server lib/lean/Init/ByCases.ilean lib/lean/Init/ByCases.olean +lib/lean/Init/ByCases.olean.private +lib/lean/Init/ByCases.olean.server lib/lean/Init/Classical.ilean lib/lean/Init/Classical.olean +lib/lean/Init/Classical.olean.private +lib/lean/Init/Classical.olean.server lib/lean/Init/Coe.ilean lib/lean/Init/Coe.olean +lib/lean/Init/Coe.olean.private +lib/lean/Init/Coe.olean.server lib/lean/Init/Control.ilean lib/lean/Init/Control.olean +lib/lean/Init/Control.olean.private +lib/lean/Init/Control.olean.server lib/lean/Init/Control/Basic.ilean lib/lean/Init/Control/Basic.olean +lib/lean/Init/Control/Basic.olean.private +lib/lean/Init/Control/Basic.olean.server lib/lean/Init/Control/EState.ilean lib/lean/Init/Control/EState.olean +lib/lean/Init/Control/EState.olean.private +lib/lean/Init/Control/EState.olean.server lib/lean/Init/Control/Except.ilean lib/lean/Init/Control/Except.olean +lib/lean/Init/Control/Except.olean.private +lib/lean/Init/Control/Except.olean.server lib/lean/Init/Control/ExceptCps.ilean lib/lean/Init/Control/ExceptCps.olean +lib/lean/Init/Control/ExceptCps.olean.private +lib/lean/Init/Control/ExceptCps.olean.server lib/lean/Init/Control/Id.ilean lib/lean/Init/Control/Id.olean +lib/lean/Init/Control/Id.olean.private +lib/lean/Init/Control/Id.olean.server lib/lean/Init/Control/Lawful.ilean lib/lean/Init/Control/Lawful.olean +lib/lean/Init/Control/Lawful.olean.private +lib/lean/Init/Control/Lawful.olean.server lib/lean/Init/Control/Lawful/Basic.ilean lib/lean/Init/Control/Lawful/Basic.olean +lib/lean/Init/Control/Lawful/Basic.olean.private +lib/lean/Init/Control/Lawful/Basic.olean.server lib/lean/Init/Control/Lawful/Instances.ilean lib/lean/Init/Control/Lawful/Instances.olean +lib/lean/Init/Control/Lawful/Instances.olean.private +lib/lean/Init/Control/Lawful/Instances.olean.server +lib/lean/Init/Control/Lawful/Lemmas.ilean +lib/lean/Init/Control/Lawful/Lemmas.olean +lib/lean/Init/Control/Lawful/Lemmas.olean.private +lib/lean/Init/Control/Lawful/Lemmas.olean.server lib/lean/Init/Control/Option.ilean lib/lean/Init/Control/Option.olean +lib/lean/Init/Control/Option.olean.private +lib/lean/Init/Control/Option.olean.server lib/lean/Init/Control/Reader.ilean lib/lean/Init/Control/Reader.olean +lib/lean/Init/Control/Reader.olean.private +lib/lean/Init/Control/Reader.olean.server lib/lean/Init/Control/State.ilean lib/lean/Init/Control/State.olean +lib/lean/Init/Control/State.olean.private +lib/lean/Init/Control/State.olean.server lib/lean/Init/Control/StateCps.ilean lib/lean/Init/Control/StateCps.olean +lib/lean/Init/Control/StateCps.olean.private +lib/lean/Init/Control/StateCps.olean.server lib/lean/Init/Control/StateRef.ilean lib/lean/Init/Control/StateRef.olean +lib/lean/Init/Control/StateRef.olean.private +lib/lean/Init/Control/StateRef.olean.server lib/lean/Init/Conv.ilean lib/lean/Init/Conv.olean +lib/lean/Init/Conv.olean.private +lib/lean/Init/Conv.olean.server lib/lean/Init/Core.ilean lib/lean/Init/Core.olean +lib/lean/Init/Core.olean.private +lib/lean/Init/Core.olean.server lib/lean/Init/Data.ilean lib/lean/Init/Data.olean +lib/lean/Init/Data.olean.private +lib/lean/Init/Data.olean.server lib/lean/Init/Data/AC.ilean lib/lean/Init/Data/AC.olean +lib/lean/Init/Data/AC.olean.private +lib/lean/Init/Data/AC.olean.server lib/lean/Init/Data/Array.ilean lib/lean/Init/Data/Array.olean +lib/lean/Init/Data/Array.olean.private +lib/lean/Init/Data/Array.olean.server lib/lean/Init/Data/Array/Attach.ilean lib/lean/Init/Data/Array/Attach.olean +lib/lean/Init/Data/Array/Attach.olean.private +lib/lean/Init/Data/Array/Attach.olean.server lib/lean/Init/Data/Array/Basic.ilean lib/lean/Init/Data/Array/Basic.olean +lib/lean/Init/Data/Array/Basic.olean.private +lib/lean/Init/Data/Array/Basic.olean.server lib/lean/Init/Data/Array/BasicAux.ilean lib/lean/Init/Data/Array/BasicAux.olean +lib/lean/Init/Data/Array/BasicAux.olean.private +lib/lean/Init/Data/Array/BasicAux.olean.server lib/lean/Init/Data/Array/BinSearch.ilean lib/lean/Init/Data/Array/BinSearch.olean +lib/lean/Init/Data/Array/BinSearch.olean.private +lib/lean/Init/Data/Array/BinSearch.olean.server +lib/lean/Init/Data/Array/Bootstrap.ilean +lib/lean/Init/Data/Array/Bootstrap.olean +lib/lean/Init/Data/Array/Bootstrap.olean.private +lib/lean/Init/Data/Array/Bootstrap.olean.server +lib/lean/Init/Data/Array/Count.ilean +lib/lean/Init/Data/Array/Count.olean +lib/lean/Init/Data/Array/Count.olean.private +lib/lean/Init/Data/Array/Count.olean.server lib/lean/Init/Data/Array/DecidableEq.ilean lib/lean/Init/Data/Array/DecidableEq.olean +lib/lean/Init/Data/Array/DecidableEq.olean.private +lib/lean/Init/Data/Array/DecidableEq.olean.server +lib/lean/Init/Data/Array/Erase.ilean +lib/lean/Init/Data/Array/Erase.olean +lib/lean/Init/Data/Array/Erase.olean.private +lib/lean/Init/Data/Array/Erase.olean.server +lib/lean/Init/Data/Array/Extract.ilean +lib/lean/Init/Data/Array/Extract.olean +lib/lean/Init/Data/Array/Extract.olean.private +lib/lean/Init/Data/Array/Extract.olean.server +lib/lean/Init/Data/Array/FinRange.ilean +lib/lean/Init/Data/Array/FinRange.olean +lib/lean/Init/Data/Array/FinRange.olean.private +lib/lean/Init/Data/Array/FinRange.olean.server +lib/lean/Init/Data/Array/Find.ilean +lib/lean/Init/Data/Array/Find.olean +lib/lean/Init/Data/Array/Find.olean.private +lib/lean/Init/Data/Array/Find.olean.server +lib/lean/Init/Data/Array/GetLit.ilean +lib/lean/Init/Data/Array/GetLit.olean +lib/lean/Init/Data/Array/GetLit.olean.private +lib/lean/Init/Data/Array/GetLit.olean.server +lib/lean/Init/Data/Array/InsertIdx.ilean +lib/lean/Init/Data/Array/InsertIdx.olean +lib/lean/Init/Data/Array/InsertIdx.olean.private +lib/lean/Init/Data/Array/InsertIdx.olean.server lib/lean/Init/Data/Array/InsertionSort.ilean lib/lean/Init/Data/Array/InsertionSort.olean +lib/lean/Init/Data/Array/InsertionSort.olean.private +lib/lean/Init/Data/Array/InsertionSort.olean.server lib/lean/Init/Data/Array/Lemmas.ilean lib/lean/Init/Data/Array/Lemmas.olean +lib/lean/Init/Data/Array/Lemmas.olean.private +lib/lean/Init/Data/Array/Lemmas.olean.server +lib/lean/Init/Data/Array/Lex.ilean +lib/lean/Init/Data/Array/Lex.olean +lib/lean/Init/Data/Array/Lex.olean.private +lib/lean/Init/Data/Array/Lex.olean.server +lib/lean/Init/Data/Array/Lex/Basic.ilean +lib/lean/Init/Data/Array/Lex/Basic.olean +lib/lean/Init/Data/Array/Lex/Basic.olean.private +lib/lean/Init/Data/Array/Lex/Basic.olean.server +lib/lean/Init/Data/Array/Lex/Lemmas.ilean +lib/lean/Init/Data/Array/Lex/Lemmas.olean +lib/lean/Init/Data/Array/Lex/Lemmas.olean.private +lib/lean/Init/Data/Array/Lex/Lemmas.olean.server +lib/lean/Init/Data/Array/MapIdx.ilean +lib/lean/Init/Data/Array/MapIdx.olean +lib/lean/Init/Data/Array/MapIdx.olean.private +lib/lean/Init/Data/Array/MapIdx.olean.server lib/lean/Init/Data/Array/Mem.ilean lib/lean/Init/Data/Array/Mem.olean +lib/lean/Init/Data/Array/Mem.olean.private +lib/lean/Init/Data/Array/Mem.olean.server +lib/lean/Init/Data/Array/Monadic.ilean +lib/lean/Init/Data/Array/Monadic.olean +lib/lean/Init/Data/Array/Monadic.olean.private +lib/lean/Init/Data/Array/Monadic.olean.server +lib/lean/Init/Data/Array/OfFn.ilean +lib/lean/Init/Data/Array/OfFn.olean +lib/lean/Init/Data/Array/OfFn.olean.private +lib/lean/Init/Data/Array/OfFn.olean.server +lib/lean/Init/Data/Array/Perm.ilean +lib/lean/Init/Data/Array/Perm.olean +lib/lean/Init/Data/Array/Perm.olean.private +lib/lean/Init/Data/Array/Perm.olean.server lib/lean/Init/Data/Array/QSort.ilean lib/lean/Init/Data/Array/QSort.olean +lib/lean/Init/Data/Array/QSort.olean.private +lib/lean/Init/Data/Array/QSort.olean.server +lib/lean/Init/Data/Array/QSort/Basic.ilean +lib/lean/Init/Data/Array/QSort/Basic.olean +lib/lean/Init/Data/Array/QSort/Basic.olean.private +lib/lean/Init/Data/Array/QSort/Basic.olean.server +lib/lean/Init/Data/Array/Range.ilean +lib/lean/Init/Data/Array/Range.olean +lib/lean/Init/Data/Array/Range.olean.private +lib/lean/Init/Data/Array/Range.olean.server +lib/lean/Init/Data/Array/Set.ilean +lib/lean/Init/Data/Array/Set.olean +lib/lean/Init/Data/Array/Set.olean.private +lib/lean/Init/Data/Array/Set.olean.server lib/lean/Init/Data/Array/Subarray.ilean lib/lean/Init/Data/Array/Subarray.olean +lib/lean/Init/Data/Array/Subarray.olean.private +lib/lean/Init/Data/Array/Subarray.olean.server lib/lean/Init/Data/Array/Subarray/Split.ilean lib/lean/Init/Data/Array/Subarray/Split.olean +lib/lean/Init/Data/Array/Subarray/Split.olean.private +lib/lean/Init/Data/Array/Subarray/Split.olean.server lib/lean/Init/Data/Array/TakeDrop.ilean lib/lean/Init/Data/Array/TakeDrop.olean +lib/lean/Init/Data/Array/TakeDrop.olean.private +lib/lean/Init/Data/Array/TakeDrop.olean.server +lib/lean/Init/Data/Array/Zip.ilean +lib/lean/Init/Data/Array/Zip.olean +lib/lean/Init/Data/Array/Zip.olean.private +lib/lean/Init/Data/Array/Zip.olean.server lib/lean/Init/Data/BEq.ilean lib/lean/Init/Data/BEq.olean +lib/lean/Init/Data/BEq.olean.private +lib/lean/Init/Data/BEq.olean.server lib/lean/Init/Data/Basic.ilean lib/lean/Init/Data/Basic.olean +lib/lean/Init/Data/Basic.olean.private +lib/lean/Init/Data/Basic.olean.server lib/lean/Init/Data/BitVec.ilean lib/lean/Init/Data/BitVec.olean +lib/lean/Init/Data/BitVec.olean.private +lib/lean/Init/Data/BitVec.olean.server lib/lean/Init/Data/BitVec/Basic.ilean lib/lean/Init/Data/BitVec/Basic.olean +lib/lean/Init/Data/BitVec/Basic.olean.private +lib/lean/Init/Data/BitVec/Basic.olean.server +lib/lean/Init/Data/BitVec/BasicAux.ilean +lib/lean/Init/Data/BitVec/BasicAux.olean +lib/lean/Init/Data/BitVec/BasicAux.olean.private +lib/lean/Init/Data/BitVec/BasicAux.olean.server lib/lean/Init/Data/BitVec/Bitblast.ilean lib/lean/Init/Data/BitVec/Bitblast.olean +lib/lean/Init/Data/BitVec/Bitblast.olean.private +lib/lean/Init/Data/BitVec/Bitblast.olean.server lib/lean/Init/Data/BitVec/Folds.ilean lib/lean/Init/Data/BitVec/Folds.olean +lib/lean/Init/Data/BitVec/Folds.olean.private +lib/lean/Init/Data/BitVec/Folds.olean.server lib/lean/Init/Data/BitVec/Lemmas.ilean lib/lean/Init/Data/BitVec/Lemmas.olean +lib/lean/Init/Data/BitVec/Lemmas.olean.private +lib/lean/Init/Data/BitVec/Lemmas.olean.server lib/lean/Init/Data/Bool.ilean lib/lean/Init/Data/Bool.olean +lib/lean/Init/Data/Bool.olean.private +lib/lean/Init/Data/Bool.olean.server lib/lean/Init/Data/ByteArray.ilean lib/lean/Init/Data/ByteArray.olean +lib/lean/Init/Data/ByteArray.olean.private +lib/lean/Init/Data/ByteArray.olean.server lib/lean/Init/Data/ByteArray/Basic.ilean lib/lean/Init/Data/ByteArray/Basic.olean +lib/lean/Init/Data/ByteArray/Basic.olean.private +lib/lean/Init/Data/ByteArray/Basic.olean.server lib/lean/Init/Data/Cast.ilean lib/lean/Init/Data/Cast.olean -lib/lean/Init/Data/Channel.ilean -lib/lean/Init/Data/Channel.olean +lib/lean/Init/Data/Cast.olean.private +lib/lean/Init/Data/Cast.olean.server lib/lean/Init/Data/Char.ilean lib/lean/Init/Data/Char.olean +lib/lean/Init/Data/Char.olean.private +lib/lean/Init/Data/Char.olean.server lib/lean/Init/Data/Char/Basic.ilean lib/lean/Init/Data/Char/Basic.olean +lib/lean/Init/Data/Char/Basic.olean.private +lib/lean/Init/Data/Char/Basic.olean.server lib/lean/Init/Data/Char/Lemmas.ilean lib/lean/Init/Data/Char/Lemmas.olean +lib/lean/Init/Data/Char/Lemmas.olean.private +lib/lean/Init/Data/Char/Lemmas.olean.server lib/lean/Init/Data/Fin.ilean lib/lean/Init/Data/Fin.olean +lib/lean/Init/Data/Fin.olean.private +lib/lean/Init/Data/Fin.olean.server lib/lean/Init/Data/Fin/Basic.ilean lib/lean/Init/Data/Fin/Basic.olean +lib/lean/Init/Data/Fin/Basic.olean.private +lib/lean/Init/Data/Fin/Basic.olean.server lib/lean/Init/Data/Fin/Bitwise.ilean lib/lean/Init/Data/Fin/Bitwise.olean +lib/lean/Init/Data/Fin/Bitwise.olean.private +lib/lean/Init/Data/Fin/Bitwise.olean.server lib/lean/Init/Data/Fin/Fold.ilean lib/lean/Init/Data/Fin/Fold.olean +lib/lean/Init/Data/Fin/Fold.olean.private +lib/lean/Init/Data/Fin/Fold.olean.server lib/lean/Init/Data/Fin/Iterate.ilean lib/lean/Init/Data/Fin/Iterate.olean +lib/lean/Init/Data/Fin/Iterate.olean.private +lib/lean/Init/Data/Fin/Iterate.olean.server lib/lean/Init/Data/Fin/Lemmas.ilean lib/lean/Init/Data/Fin/Lemmas.olean +lib/lean/Init/Data/Fin/Lemmas.olean.private +lib/lean/Init/Data/Fin/Lemmas.olean.server lib/lean/Init/Data/Fin/Log2.ilean lib/lean/Init/Data/Fin/Log2.olean +lib/lean/Init/Data/Fin/Log2.olean.private +lib/lean/Init/Data/Fin/Log2.olean.server lib/lean/Init/Data/Float.ilean lib/lean/Init/Data/Float.olean +lib/lean/Init/Data/Float.olean.private +lib/lean/Init/Data/Float.olean.server +lib/lean/Init/Data/Float32.ilean +lib/lean/Init/Data/Float32.olean +lib/lean/Init/Data/Float32.olean.private +lib/lean/Init/Data/Float32.olean.server lib/lean/Init/Data/FloatArray.ilean lib/lean/Init/Data/FloatArray.olean +lib/lean/Init/Data/FloatArray.olean.private +lib/lean/Init/Data/FloatArray.olean.server lib/lean/Init/Data/FloatArray/Basic.ilean lib/lean/Init/Data/FloatArray/Basic.olean +lib/lean/Init/Data/FloatArray/Basic.olean.private +lib/lean/Init/Data/FloatArray/Basic.olean.server lib/lean/Init/Data/Format.ilean lib/lean/Init/Data/Format.olean +lib/lean/Init/Data/Format.olean.private +lib/lean/Init/Data/Format.olean.server lib/lean/Init/Data/Format/Basic.ilean lib/lean/Init/Data/Format/Basic.olean +lib/lean/Init/Data/Format/Basic.olean.private +lib/lean/Init/Data/Format/Basic.olean.server lib/lean/Init/Data/Format/Instances.ilean lib/lean/Init/Data/Format/Instances.olean +lib/lean/Init/Data/Format/Instances.olean.private +lib/lean/Init/Data/Format/Instances.olean.server lib/lean/Init/Data/Format/Macro.ilean lib/lean/Init/Data/Format/Macro.olean +lib/lean/Init/Data/Format/Macro.olean.private +lib/lean/Init/Data/Format/Macro.olean.server lib/lean/Init/Data/Format/Syntax.ilean lib/lean/Init/Data/Format/Syntax.olean +lib/lean/Init/Data/Format/Syntax.olean.private +lib/lean/Init/Data/Format/Syntax.olean.server +lib/lean/Init/Data/Function.ilean +lib/lean/Init/Data/Function.olean +lib/lean/Init/Data/Function.olean.private +lib/lean/Init/Data/Function.olean.server lib/lean/Init/Data/Hashable.ilean lib/lean/Init/Data/Hashable.olean +lib/lean/Init/Data/Hashable.olean.private +lib/lean/Init/Data/Hashable.olean.server lib/lean/Init/Data/Int.ilean lib/lean/Init/Data/Int.olean +lib/lean/Init/Data/Int.olean.private +lib/lean/Init/Data/Int.olean.server lib/lean/Init/Data/Int/Basic.ilean lib/lean/Init/Data/Int/Basic.olean +lib/lean/Init/Data/Int/Basic.olean.private +lib/lean/Init/Data/Int/Basic.olean.server lib/lean/Init/Data/Int/Bitwise.ilean lib/lean/Init/Data/Int/Bitwise.olean +lib/lean/Init/Data/Int/Bitwise.olean.private +lib/lean/Init/Data/Int/Bitwise.olean.server +lib/lean/Init/Data/Int/Bitwise/Basic.ilean +lib/lean/Init/Data/Int/Bitwise/Basic.olean +lib/lean/Init/Data/Int/Bitwise/Basic.olean.private +lib/lean/Init/Data/Int/Bitwise/Basic.olean.server lib/lean/Init/Data/Int/Bitwise/Lemmas.ilean lib/lean/Init/Data/Int/Bitwise/Lemmas.olean +lib/lean/Init/Data/Int/Bitwise/Lemmas.olean.private +lib/lean/Init/Data/Int/Bitwise/Lemmas.olean.server +lib/lean/Init/Data/Int/Compare.ilean +lib/lean/Init/Data/Int/Compare.olean +lib/lean/Init/Data/Int/Compare.olean.private +lib/lean/Init/Data/Int/Compare.olean.server +lib/lean/Init/Data/Int/Cooper.ilean +lib/lean/Init/Data/Int/Cooper.olean +lib/lean/Init/Data/Int/Cooper.olean.private +lib/lean/Init/Data/Int/Cooper.olean.server lib/lean/Init/Data/Int/DivMod.ilean lib/lean/Init/Data/Int/DivMod.olean -lib/lean/Init/Data/Int/DivModLemmas.ilean -lib/lean/Init/Data/Int/DivModLemmas.olean +lib/lean/Init/Data/Int/DivMod.olean.private +lib/lean/Init/Data/Int/DivMod.olean.server +lib/lean/Init/Data/Int/DivMod/Basic.ilean +lib/lean/Init/Data/Int/DivMod/Basic.olean +lib/lean/Init/Data/Int/DivMod/Basic.olean.private +lib/lean/Init/Data/Int/DivMod/Basic.olean.server +lib/lean/Init/Data/Int/DivMod/Bootstrap.ilean +lib/lean/Init/Data/Int/DivMod/Bootstrap.olean +lib/lean/Init/Data/Int/DivMod/Bootstrap.olean.private +lib/lean/Init/Data/Int/DivMod/Bootstrap.olean.server +lib/lean/Init/Data/Int/DivMod/Lemmas.ilean +lib/lean/Init/Data/Int/DivMod/Lemmas.olean +lib/lean/Init/Data/Int/DivMod/Lemmas.olean.private +lib/lean/Init/Data/Int/DivMod/Lemmas.olean.server lib/lean/Init/Data/Int/Gcd.ilean lib/lean/Init/Data/Int/Gcd.olean +lib/lean/Init/Data/Int/Gcd.olean.private +lib/lean/Init/Data/Int/Gcd.olean.server lib/lean/Init/Data/Int/Lemmas.ilean lib/lean/Init/Data/Int/Lemmas.olean +lib/lean/Init/Data/Int/Lemmas.olean.private +lib/lean/Init/Data/Int/Lemmas.olean.server lib/lean/Init/Data/Int/LemmasAux.ilean lib/lean/Init/Data/Int/LemmasAux.olean +lib/lean/Init/Data/Int/LemmasAux.olean.private +lib/lean/Init/Data/Int/LemmasAux.olean.server +lib/lean/Init/Data/Int/Linear.ilean +lib/lean/Init/Data/Int/Linear.olean +lib/lean/Init/Data/Int/Linear.olean.private +lib/lean/Init/Data/Int/Linear.olean.server +lib/lean/Init/Data/Int/OfNat.ilean +lib/lean/Init/Data/Int/OfNat.olean +lib/lean/Init/Data/Int/OfNat.olean.private +lib/lean/Init/Data/Int/OfNat.olean.server lib/lean/Init/Data/Int/Order.ilean lib/lean/Init/Data/Int/Order.olean +lib/lean/Init/Data/Int/Order.olean.private +lib/lean/Init/Data/Int/Order.olean.server lib/lean/Init/Data/Int/Pow.ilean lib/lean/Init/Data/Int/Pow.olean +lib/lean/Init/Data/Int/Pow.olean.private +lib/lean/Init/Data/Int/Pow.olean.server lib/lean/Init/Data/List.ilean lib/lean/Init/Data/List.olean +lib/lean/Init/Data/List.olean.private +lib/lean/Init/Data/List.olean.server lib/lean/Init/Data/List/Attach.ilean lib/lean/Init/Data/List/Attach.olean +lib/lean/Init/Data/List/Attach.olean.private +lib/lean/Init/Data/List/Attach.olean.server lib/lean/Init/Data/List/Basic.ilean lib/lean/Init/Data/List/Basic.olean +lib/lean/Init/Data/List/Basic.olean.private +lib/lean/Init/Data/List/Basic.olean.server lib/lean/Init/Data/List/BasicAux.ilean lib/lean/Init/Data/List/BasicAux.olean +lib/lean/Init/Data/List/BasicAux.olean.private +lib/lean/Init/Data/List/BasicAux.olean.server lib/lean/Init/Data/List/Control.ilean lib/lean/Init/Data/List/Control.olean +lib/lean/Init/Data/List/Control.olean.private +lib/lean/Init/Data/List/Control.olean.server lib/lean/Init/Data/List/Count.ilean lib/lean/Init/Data/List/Count.olean +lib/lean/Init/Data/List/Count.olean.private +lib/lean/Init/Data/List/Count.olean.server lib/lean/Init/Data/List/Erase.ilean lib/lean/Init/Data/List/Erase.olean +lib/lean/Init/Data/List/Erase.olean.private +lib/lean/Init/Data/List/Erase.olean.server +lib/lean/Init/Data/List/FinRange.ilean +lib/lean/Init/Data/List/FinRange.olean +lib/lean/Init/Data/List/FinRange.olean.private +lib/lean/Init/Data/List/FinRange.olean.server lib/lean/Init/Data/List/Find.ilean lib/lean/Init/Data/List/Find.olean +lib/lean/Init/Data/List/Find.olean.private +lib/lean/Init/Data/List/Find.olean.server lib/lean/Init/Data/List/Impl.ilean lib/lean/Init/Data/List/Impl.olean +lib/lean/Init/Data/List/Impl.olean.private +lib/lean/Init/Data/List/Impl.olean.server lib/lean/Init/Data/List/Lemmas.ilean lib/lean/Init/Data/List/Lemmas.olean +lib/lean/Init/Data/List/Lemmas.olean.private +lib/lean/Init/Data/List/Lemmas.olean.server +lib/lean/Init/Data/List/Lex.ilean +lib/lean/Init/Data/List/Lex.olean +lib/lean/Init/Data/List/Lex.olean.private +lib/lean/Init/Data/List/Lex.olean.server +lib/lean/Init/Data/List/MapIdx.ilean +lib/lean/Init/Data/List/MapIdx.olean +lib/lean/Init/Data/List/MapIdx.olean.private +lib/lean/Init/Data/List/MapIdx.olean.server lib/lean/Init/Data/List/MinMax.ilean lib/lean/Init/Data/List/MinMax.olean +lib/lean/Init/Data/List/MinMax.olean.private +lib/lean/Init/Data/List/MinMax.olean.server lib/lean/Init/Data/List/Monadic.ilean lib/lean/Init/Data/List/Monadic.olean +lib/lean/Init/Data/List/Monadic.olean.private +lib/lean/Init/Data/List/Monadic.olean.server lib/lean/Init/Data/List/Nat.ilean lib/lean/Init/Data/List/Nat.olean +lib/lean/Init/Data/List/Nat.olean.private +lib/lean/Init/Data/List/Nat.olean.server +lib/lean/Init/Data/List/Nat/BEq.ilean +lib/lean/Init/Data/List/Nat/BEq.olean +lib/lean/Init/Data/List/Nat/BEq.olean.private +lib/lean/Init/Data/List/Nat/BEq.olean.server lib/lean/Init/Data/List/Nat/Basic.ilean lib/lean/Init/Data/List/Nat/Basic.olean +lib/lean/Init/Data/List/Nat/Basic.olean.private +lib/lean/Init/Data/List/Nat/Basic.olean.server +lib/lean/Init/Data/List/Nat/Count.ilean +lib/lean/Init/Data/List/Nat/Count.olean +lib/lean/Init/Data/List/Nat/Count.olean.private +lib/lean/Init/Data/List/Nat/Count.olean.server +lib/lean/Init/Data/List/Nat/Erase.ilean +lib/lean/Init/Data/List/Nat/Erase.olean +lib/lean/Init/Data/List/Nat/Erase.olean.private +lib/lean/Init/Data/List/Nat/Erase.olean.server +lib/lean/Init/Data/List/Nat/Find.ilean +lib/lean/Init/Data/List/Nat/Find.olean +lib/lean/Init/Data/List/Nat/Find.olean.private +lib/lean/Init/Data/List/Nat/Find.olean.server +lib/lean/Init/Data/List/Nat/InsertIdx.ilean +lib/lean/Init/Data/List/Nat/InsertIdx.olean +lib/lean/Init/Data/List/Nat/InsertIdx.olean.private +lib/lean/Init/Data/List/Nat/InsertIdx.olean.server +lib/lean/Init/Data/List/Nat/Modify.ilean +lib/lean/Init/Data/List/Nat/Modify.olean +lib/lean/Init/Data/List/Nat/Modify.olean.private +lib/lean/Init/Data/List/Nat/Modify.olean.server lib/lean/Init/Data/List/Nat/Pairwise.ilean lib/lean/Init/Data/List/Nat/Pairwise.olean +lib/lean/Init/Data/List/Nat/Pairwise.olean.private +lib/lean/Init/Data/List/Nat/Pairwise.olean.server +lib/lean/Init/Data/List/Nat/Perm.ilean +lib/lean/Init/Data/List/Nat/Perm.olean +lib/lean/Init/Data/List/Nat/Perm.olean.private +lib/lean/Init/Data/List/Nat/Perm.olean.server lib/lean/Init/Data/List/Nat/Range.ilean lib/lean/Init/Data/List/Nat/Range.olean +lib/lean/Init/Data/List/Nat/Range.olean.private +lib/lean/Init/Data/List/Nat/Range.olean.server lib/lean/Init/Data/List/Nat/Sublist.ilean lib/lean/Init/Data/List/Nat/Sublist.olean +lib/lean/Init/Data/List/Nat/Sublist.olean.private +lib/lean/Init/Data/List/Nat/Sublist.olean.server lib/lean/Init/Data/List/Nat/TakeDrop.ilean lib/lean/Init/Data/List/Nat/TakeDrop.olean +lib/lean/Init/Data/List/Nat/TakeDrop.olean.private +lib/lean/Init/Data/List/Nat/TakeDrop.olean.server lib/lean/Init/Data/List/Notation.ilean lib/lean/Init/Data/List/Notation.olean +lib/lean/Init/Data/List/Notation.olean.private +lib/lean/Init/Data/List/Notation.olean.server +lib/lean/Init/Data/List/OfFn.ilean +lib/lean/Init/Data/List/OfFn.olean +lib/lean/Init/Data/List/OfFn.olean.private +lib/lean/Init/Data/List/OfFn.olean.server lib/lean/Init/Data/List/Pairwise.ilean lib/lean/Init/Data/List/Pairwise.olean +lib/lean/Init/Data/List/Pairwise.olean.private +lib/lean/Init/Data/List/Pairwise.olean.server lib/lean/Init/Data/List/Perm.ilean lib/lean/Init/Data/List/Perm.olean +lib/lean/Init/Data/List/Perm.olean.private +lib/lean/Init/Data/List/Perm.olean.server lib/lean/Init/Data/List/Range.ilean lib/lean/Init/Data/List/Range.olean +lib/lean/Init/Data/List/Range.olean.private +lib/lean/Init/Data/List/Range.olean.server lib/lean/Init/Data/List/Sort.ilean lib/lean/Init/Data/List/Sort.olean +lib/lean/Init/Data/List/Sort.olean.private +lib/lean/Init/Data/List/Sort.olean.server lib/lean/Init/Data/List/Sort/Basic.ilean lib/lean/Init/Data/List/Sort/Basic.olean +lib/lean/Init/Data/List/Sort/Basic.olean.private +lib/lean/Init/Data/List/Sort/Basic.olean.server lib/lean/Init/Data/List/Sort/Impl.ilean lib/lean/Init/Data/List/Sort/Impl.olean +lib/lean/Init/Data/List/Sort/Impl.olean.private +lib/lean/Init/Data/List/Sort/Impl.olean.server lib/lean/Init/Data/List/Sort/Lemmas.ilean lib/lean/Init/Data/List/Sort/Lemmas.olean +lib/lean/Init/Data/List/Sort/Lemmas.olean.private +lib/lean/Init/Data/List/Sort/Lemmas.olean.server lib/lean/Init/Data/List/Sublist.ilean lib/lean/Init/Data/List/Sublist.olean +lib/lean/Init/Data/List/Sublist.olean.private +lib/lean/Init/Data/List/Sublist.olean.server lib/lean/Init/Data/List/TakeDrop.ilean lib/lean/Init/Data/List/TakeDrop.olean +lib/lean/Init/Data/List/TakeDrop.olean.private +lib/lean/Init/Data/List/TakeDrop.olean.server +lib/lean/Init/Data/List/ToArray.ilean +lib/lean/Init/Data/List/ToArray.olean +lib/lean/Init/Data/List/ToArray.olean.private +lib/lean/Init/Data/List/ToArray.olean.server +lib/lean/Init/Data/List/ToArrayImpl.ilean +lib/lean/Init/Data/List/ToArrayImpl.olean +lib/lean/Init/Data/List/ToArrayImpl.olean.private +lib/lean/Init/Data/List/ToArrayImpl.olean.server lib/lean/Init/Data/List/Zip.ilean lib/lean/Init/Data/List/Zip.olean +lib/lean/Init/Data/List/Zip.olean.private +lib/lean/Init/Data/List/Zip.olean.server lib/lean/Init/Data/Nat.ilean lib/lean/Init/Data/Nat.olean +lib/lean/Init/Data/Nat.olean.private +lib/lean/Init/Data/Nat.olean.server lib/lean/Init/Data/Nat/Basic.ilean lib/lean/Init/Data/Nat/Basic.olean +lib/lean/Init/Data/Nat/Basic.olean.private +lib/lean/Init/Data/Nat/Basic.olean.server lib/lean/Init/Data/Nat/Bitwise.ilean lib/lean/Init/Data/Nat/Bitwise.olean +lib/lean/Init/Data/Nat/Bitwise.olean.private +lib/lean/Init/Data/Nat/Bitwise.olean.server lib/lean/Init/Data/Nat/Bitwise/Basic.ilean lib/lean/Init/Data/Nat/Bitwise/Basic.olean +lib/lean/Init/Data/Nat/Bitwise/Basic.olean.private +lib/lean/Init/Data/Nat/Bitwise/Basic.olean.server lib/lean/Init/Data/Nat/Bitwise/Lemmas.ilean lib/lean/Init/Data/Nat/Bitwise/Lemmas.olean +lib/lean/Init/Data/Nat/Bitwise/Lemmas.olean.private +lib/lean/Init/Data/Nat/Bitwise/Lemmas.olean.server lib/lean/Init/Data/Nat/Compare.ilean lib/lean/Init/Data/Nat/Compare.olean +lib/lean/Init/Data/Nat/Compare.olean.private +lib/lean/Init/Data/Nat/Compare.olean.server lib/lean/Init/Data/Nat/Control.ilean lib/lean/Init/Data/Nat/Control.olean +lib/lean/Init/Data/Nat/Control.olean.private +lib/lean/Init/Data/Nat/Control.olean.server lib/lean/Init/Data/Nat/Div.ilean lib/lean/Init/Data/Nat/Div.olean +lib/lean/Init/Data/Nat/Div.olean.private +lib/lean/Init/Data/Nat/Div.olean.server +lib/lean/Init/Data/Nat/Div/Basic.ilean +lib/lean/Init/Data/Nat/Div/Basic.olean +lib/lean/Init/Data/Nat/Div/Basic.olean.private +lib/lean/Init/Data/Nat/Div/Basic.olean.server +lib/lean/Init/Data/Nat/Div/Lemmas.ilean +lib/lean/Init/Data/Nat/Div/Lemmas.olean +lib/lean/Init/Data/Nat/Div/Lemmas.olean.private +lib/lean/Init/Data/Nat/Div/Lemmas.olean.server lib/lean/Init/Data/Nat/Dvd.ilean lib/lean/Init/Data/Nat/Dvd.olean +lib/lean/Init/Data/Nat/Dvd.olean.private +lib/lean/Init/Data/Nat/Dvd.olean.server +lib/lean/Init/Data/Nat/Fold.ilean +lib/lean/Init/Data/Nat/Fold.olean +lib/lean/Init/Data/Nat/Fold.olean.private +lib/lean/Init/Data/Nat/Fold.olean.server lib/lean/Init/Data/Nat/Gcd.ilean lib/lean/Init/Data/Nat/Gcd.olean +lib/lean/Init/Data/Nat/Gcd.olean.private +lib/lean/Init/Data/Nat/Gcd.olean.server lib/lean/Init/Data/Nat/Lcm.ilean lib/lean/Init/Data/Nat/Lcm.olean +lib/lean/Init/Data/Nat/Lcm.olean.private +lib/lean/Init/Data/Nat/Lcm.olean.server lib/lean/Init/Data/Nat/Lemmas.ilean lib/lean/Init/Data/Nat/Lemmas.olean +lib/lean/Init/Data/Nat/Lemmas.olean.private +lib/lean/Init/Data/Nat/Lemmas.olean.server lib/lean/Init/Data/Nat/Linear.ilean lib/lean/Init/Data/Nat/Linear.olean +lib/lean/Init/Data/Nat/Linear.olean.private +lib/lean/Init/Data/Nat/Linear.olean.server lib/lean/Init/Data/Nat/Log2.ilean lib/lean/Init/Data/Nat/Log2.olean +lib/lean/Init/Data/Nat/Log2.olean.private +lib/lean/Init/Data/Nat/Log2.olean.server lib/lean/Init/Data/Nat/MinMax.ilean lib/lean/Init/Data/Nat/MinMax.olean +lib/lean/Init/Data/Nat/MinMax.olean.private +lib/lean/Init/Data/Nat/MinMax.olean.server lib/lean/Init/Data/Nat/Mod.ilean lib/lean/Init/Data/Nat/Mod.olean +lib/lean/Init/Data/Nat/Mod.olean.private +lib/lean/Init/Data/Nat/Mod.olean.server lib/lean/Init/Data/Nat/Power2.ilean lib/lean/Init/Data/Nat/Power2.olean +lib/lean/Init/Data/Nat/Power2.olean.private +lib/lean/Init/Data/Nat/Power2.olean.server lib/lean/Init/Data/Nat/SOM.ilean lib/lean/Init/Data/Nat/SOM.olean +lib/lean/Init/Data/Nat/SOM.olean.private +lib/lean/Init/Data/Nat/SOM.olean.server lib/lean/Init/Data/Nat/Simproc.ilean lib/lean/Init/Data/Nat/Simproc.olean +lib/lean/Init/Data/Nat/Simproc.olean.private +lib/lean/Init/Data/Nat/Simproc.olean.server +lib/lean/Init/Data/NeZero.ilean +lib/lean/Init/Data/NeZero.olean +lib/lean/Init/Data/NeZero.olean.private +lib/lean/Init/Data/NeZero.olean.server lib/lean/Init/Data/OfScientific.ilean lib/lean/Init/Data/OfScientific.olean +lib/lean/Init/Data/OfScientific.olean.private +lib/lean/Init/Data/OfScientific.olean.server lib/lean/Init/Data/Option.ilean lib/lean/Init/Data/Option.olean +lib/lean/Init/Data/Option.olean.private +lib/lean/Init/Data/Option.olean.server +lib/lean/Init/Data/Option/Attach.ilean +lib/lean/Init/Data/Option/Attach.olean +lib/lean/Init/Data/Option/Attach.olean.private +lib/lean/Init/Data/Option/Attach.olean.server lib/lean/Init/Data/Option/Basic.ilean lib/lean/Init/Data/Option/Basic.olean +lib/lean/Init/Data/Option/Basic.olean.private +lib/lean/Init/Data/Option/Basic.olean.server lib/lean/Init/Data/Option/BasicAux.ilean lib/lean/Init/Data/Option/BasicAux.olean +lib/lean/Init/Data/Option/BasicAux.olean.private +lib/lean/Init/Data/Option/BasicAux.olean.server +lib/lean/Init/Data/Option/Coe.ilean +lib/lean/Init/Data/Option/Coe.olean +lib/lean/Init/Data/Option/Coe.olean.private +lib/lean/Init/Data/Option/Coe.olean.server lib/lean/Init/Data/Option/Instances.ilean lib/lean/Init/Data/Option/Instances.olean +lib/lean/Init/Data/Option/Instances.olean.private +lib/lean/Init/Data/Option/Instances.olean.server lib/lean/Init/Data/Option/Lemmas.ilean lib/lean/Init/Data/Option/Lemmas.olean +lib/lean/Init/Data/Option/Lemmas.olean.private +lib/lean/Init/Data/Option/Lemmas.olean.server +lib/lean/Init/Data/Option/List.ilean +lib/lean/Init/Data/Option/List.olean +lib/lean/Init/Data/Option/List.olean.private +lib/lean/Init/Data/Option/List.olean.server +lib/lean/Init/Data/Option/Monadic.ilean +lib/lean/Init/Data/Option/Monadic.olean +lib/lean/Init/Data/Option/Monadic.olean.private +lib/lean/Init/Data/Option/Monadic.olean.server lib/lean/Init/Data/Ord.ilean lib/lean/Init/Data/Ord.olean +lib/lean/Init/Data/Ord.olean.private +lib/lean/Init/Data/Ord.olean.server lib/lean/Init/Data/PLift.ilean lib/lean/Init/Data/PLift.olean +lib/lean/Init/Data/PLift.olean.private +lib/lean/Init/Data/PLift.olean.server lib/lean/Init/Data/Prod.ilean lib/lean/Init/Data/Prod.olean +lib/lean/Init/Data/Prod.olean.private +lib/lean/Init/Data/Prod.olean.server lib/lean/Init/Data/Queue.ilean lib/lean/Init/Data/Queue.olean +lib/lean/Init/Data/Queue.olean.private +lib/lean/Init/Data/Queue.olean.server +lib/lean/Init/Data/RArray.ilean +lib/lean/Init/Data/RArray.olean +lib/lean/Init/Data/RArray.olean.private +lib/lean/Init/Data/RArray.olean.server lib/lean/Init/Data/Random.ilean lib/lean/Init/Data/Random.olean +lib/lean/Init/Data/Random.olean.private +lib/lean/Init/Data/Random.olean.server lib/lean/Init/Data/Range.ilean lib/lean/Init/Data/Range.olean +lib/lean/Init/Data/Range.olean.private +lib/lean/Init/Data/Range.olean.server +lib/lean/Init/Data/Range/Basic.ilean +lib/lean/Init/Data/Range/Basic.olean +lib/lean/Init/Data/Range/Basic.olean.private +lib/lean/Init/Data/Range/Basic.olean.server +lib/lean/Init/Data/Range/Lemmas.ilean +lib/lean/Init/Data/Range/Lemmas.olean +lib/lean/Init/Data/Range/Lemmas.olean.private +lib/lean/Init/Data/Range/Lemmas.olean.server lib/lean/Init/Data/Repr.ilean lib/lean/Init/Data/Repr.olean +lib/lean/Init/Data/Repr.olean.private +lib/lean/Init/Data/Repr.olean.server +lib/lean/Init/Data/SInt.ilean +lib/lean/Init/Data/SInt.olean +lib/lean/Init/Data/SInt.olean.private +lib/lean/Init/Data/SInt.olean.server +lib/lean/Init/Data/SInt/Basic.ilean +lib/lean/Init/Data/SInt/Basic.olean +lib/lean/Init/Data/SInt/Basic.olean.private +lib/lean/Init/Data/SInt/Basic.olean.server +lib/lean/Init/Data/SInt/Bitwise.ilean +lib/lean/Init/Data/SInt/Bitwise.olean +lib/lean/Init/Data/SInt/Bitwise.olean.private +lib/lean/Init/Data/SInt/Bitwise.olean.server +lib/lean/Init/Data/SInt/Float.ilean +lib/lean/Init/Data/SInt/Float.olean +lib/lean/Init/Data/SInt/Float.olean.private +lib/lean/Init/Data/SInt/Float.olean.server +lib/lean/Init/Data/SInt/Float32.ilean +lib/lean/Init/Data/SInt/Float32.olean +lib/lean/Init/Data/SInt/Float32.olean.private +lib/lean/Init/Data/SInt/Float32.olean.server +lib/lean/Init/Data/SInt/Lemmas.ilean +lib/lean/Init/Data/SInt/Lemmas.olean +lib/lean/Init/Data/SInt/Lemmas.olean.private +lib/lean/Init/Data/SInt/Lemmas.olean.server lib/lean/Init/Data/Stream.ilean lib/lean/Init/Data/Stream.olean +lib/lean/Init/Data/Stream.olean.private +lib/lean/Init/Data/Stream.olean.server lib/lean/Init/Data/String.ilean lib/lean/Init/Data/String.olean +lib/lean/Init/Data/String.olean.private +lib/lean/Init/Data/String.olean.server lib/lean/Init/Data/String/Basic.ilean lib/lean/Init/Data/String/Basic.olean +lib/lean/Init/Data/String/Basic.olean.private +lib/lean/Init/Data/String/Basic.olean.server lib/lean/Init/Data/String/Extra.ilean lib/lean/Init/Data/String/Extra.olean +lib/lean/Init/Data/String/Extra.olean.private +lib/lean/Init/Data/String/Extra.olean.server lib/lean/Init/Data/String/Lemmas.ilean lib/lean/Init/Data/String/Lemmas.olean +lib/lean/Init/Data/String/Lemmas.olean.private +lib/lean/Init/Data/String/Lemmas.olean.server lib/lean/Init/Data/Subtype.ilean lib/lean/Init/Data/Subtype.olean +lib/lean/Init/Data/Subtype.olean.private +lib/lean/Init/Data/Subtype.olean.server lib/lean/Init/Data/Sum.ilean lib/lean/Init/Data/Sum.olean +lib/lean/Init/Data/Sum.olean.private +lib/lean/Init/Data/Sum.olean.server +lib/lean/Init/Data/Sum/Basic.ilean +lib/lean/Init/Data/Sum/Basic.olean +lib/lean/Init/Data/Sum/Basic.olean.private +lib/lean/Init/Data/Sum/Basic.olean.server +lib/lean/Init/Data/Sum/Lemmas.ilean +lib/lean/Init/Data/Sum/Lemmas.olean +lib/lean/Init/Data/Sum/Lemmas.olean.private +lib/lean/Init/Data/Sum/Lemmas.olean.server lib/lean/Init/Data/ToString.ilean lib/lean/Init/Data/ToString.olean +lib/lean/Init/Data/ToString.olean.private +lib/lean/Init/Data/ToString.olean.server lib/lean/Init/Data/ToString/Basic.ilean lib/lean/Init/Data/ToString/Basic.olean +lib/lean/Init/Data/ToString/Basic.olean.private +lib/lean/Init/Data/ToString/Basic.olean.server lib/lean/Init/Data/ToString/Macro.ilean lib/lean/Init/Data/ToString/Macro.olean +lib/lean/Init/Data/ToString/Macro.olean.private +lib/lean/Init/Data/ToString/Macro.olean.server lib/lean/Init/Data/UInt.ilean lib/lean/Init/Data/UInt.olean +lib/lean/Init/Data/UInt.olean.private +lib/lean/Init/Data/UInt.olean.server lib/lean/Init/Data/UInt/Basic.ilean lib/lean/Init/Data/UInt/Basic.olean +lib/lean/Init/Data/UInt/Basic.olean.private +lib/lean/Init/Data/UInt/Basic.olean.server +lib/lean/Init/Data/UInt/BasicAux.ilean +lib/lean/Init/Data/UInt/BasicAux.olean +lib/lean/Init/Data/UInt/BasicAux.olean.private +lib/lean/Init/Data/UInt/BasicAux.olean.server lib/lean/Init/Data/UInt/Bitwise.ilean lib/lean/Init/Data/UInt/Bitwise.olean +lib/lean/Init/Data/UInt/Bitwise.olean.private +lib/lean/Init/Data/UInt/Bitwise.olean.server lib/lean/Init/Data/UInt/Lemmas.ilean lib/lean/Init/Data/UInt/Lemmas.olean +lib/lean/Init/Data/UInt/Lemmas.olean.private +lib/lean/Init/Data/UInt/Lemmas.olean.server lib/lean/Init/Data/UInt/Log2.ilean lib/lean/Init/Data/UInt/Log2.olean +lib/lean/Init/Data/UInt/Log2.olean.private +lib/lean/Init/Data/UInt/Log2.olean.server lib/lean/Init/Data/ULift.ilean lib/lean/Init/Data/ULift.olean +lib/lean/Init/Data/ULift.olean.private +lib/lean/Init/Data/ULift.olean.server +lib/lean/Init/Data/Vector.ilean +lib/lean/Init/Data/Vector.olean +lib/lean/Init/Data/Vector.olean.private +lib/lean/Init/Data/Vector.olean.server +lib/lean/Init/Data/Vector/Attach.ilean +lib/lean/Init/Data/Vector/Attach.olean +lib/lean/Init/Data/Vector/Attach.olean.private +lib/lean/Init/Data/Vector/Attach.olean.server +lib/lean/Init/Data/Vector/Basic.ilean +lib/lean/Init/Data/Vector/Basic.olean +lib/lean/Init/Data/Vector/Basic.olean.private +lib/lean/Init/Data/Vector/Basic.olean.server +lib/lean/Init/Data/Vector/Count.ilean +lib/lean/Init/Data/Vector/Count.olean +lib/lean/Init/Data/Vector/Count.olean.private +lib/lean/Init/Data/Vector/Count.olean.server +lib/lean/Init/Data/Vector/DecidableEq.ilean +lib/lean/Init/Data/Vector/DecidableEq.olean +lib/lean/Init/Data/Vector/DecidableEq.olean.private +lib/lean/Init/Data/Vector/DecidableEq.olean.server +lib/lean/Init/Data/Vector/Erase.ilean +lib/lean/Init/Data/Vector/Erase.olean +lib/lean/Init/Data/Vector/Erase.olean.private +lib/lean/Init/Data/Vector/Erase.olean.server +lib/lean/Init/Data/Vector/Extract.ilean +lib/lean/Init/Data/Vector/Extract.olean +lib/lean/Init/Data/Vector/Extract.olean.private +lib/lean/Init/Data/Vector/Extract.olean.server +lib/lean/Init/Data/Vector/FinRange.ilean +lib/lean/Init/Data/Vector/FinRange.olean +lib/lean/Init/Data/Vector/FinRange.olean.private +lib/lean/Init/Data/Vector/FinRange.olean.server +lib/lean/Init/Data/Vector/Find.ilean +lib/lean/Init/Data/Vector/Find.olean +lib/lean/Init/Data/Vector/Find.olean.private +lib/lean/Init/Data/Vector/Find.olean.server +lib/lean/Init/Data/Vector/InsertIdx.ilean +lib/lean/Init/Data/Vector/InsertIdx.olean +lib/lean/Init/Data/Vector/InsertIdx.olean.private +lib/lean/Init/Data/Vector/InsertIdx.olean.server +lib/lean/Init/Data/Vector/Lemmas.ilean +lib/lean/Init/Data/Vector/Lemmas.olean +lib/lean/Init/Data/Vector/Lemmas.olean.private +lib/lean/Init/Data/Vector/Lemmas.olean.server +lib/lean/Init/Data/Vector/Lex.ilean +lib/lean/Init/Data/Vector/Lex.olean +lib/lean/Init/Data/Vector/Lex.olean.private +lib/lean/Init/Data/Vector/Lex.olean.server +lib/lean/Init/Data/Vector/MapIdx.ilean +lib/lean/Init/Data/Vector/MapIdx.olean +lib/lean/Init/Data/Vector/MapIdx.olean.private +lib/lean/Init/Data/Vector/MapIdx.olean.server +lib/lean/Init/Data/Vector/Monadic.ilean +lib/lean/Init/Data/Vector/Monadic.olean +lib/lean/Init/Data/Vector/Monadic.olean.private +lib/lean/Init/Data/Vector/Monadic.olean.server +lib/lean/Init/Data/Vector/OfFn.ilean +lib/lean/Init/Data/Vector/OfFn.olean +lib/lean/Init/Data/Vector/OfFn.olean.private +lib/lean/Init/Data/Vector/OfFn.olean.server +lib/lean/Init/Data/Vector/Perm.ilean +lib/lean/Init/Data/Vector/Perm.olean +lib/lean/Init/Data/Vector/Perm.olean.private +lib/lean/Init/Data/Vector/Perm.olean.server +lib/lean/Init/Data/Vector/Range.ilean +lib/lean/Init/Data/Vector/Range.olean +lib/lean/Init/Data/Vector/Range.olean.private +lib/lean/Init/Data/Vector/Range.olean.server +lib/lean/Init/Data/Vector/Zip.ilean +lib/lean/Init/Data/Vector/Zip.olean +lib/lean/Init/Data/Vector/Zip.olean.private +lib/lean/Init/Data/Vector/Zip.olean.server +lib/lean/Init/Data/Zero.ilean +lib/lean/Init/Data/Zero.olean +lib/lean/Init/Data/Zero.olean.private +lib/lean/Init/Data/Zero.olean.server lib/lean/Init/Dynamic.ilean lib/lean/Init/Dynamic.olean +lib/lean/Init/Dynamic.olean.private +lib/lean/Init/Dynamic.olean.server lib/lean/Init/Ext.ilean lib/lean/Init/Ext.olean +lib/lean/Init/Ext.olean.private +lib/lean/Init/Ext.olean.server lib/lean/Init/GetElem.ilean lib/lean/Init/GetElem.olean +lib/lean/Init/GetElem.olean.private +lib/lean/Init/GetElem.olean.server lib/lean/Init/Grind.ilean lib/lean/Init/Grind.olean +lib/lean/Init/Grind.olean.private +lib/lean/Init/Grind.olean.server lib/lean/Init/Grind/Cases.ilean lib/lean/Init/Grind/Cases.olean +lib/lean/Init/Grind/Cases.olean.private +lib/lean/Init/Grind/Cases.olean.server +lib/lean/Init/Grind/CommRing.ilean +lib/lean/Init/Grind/CommRing.olean +lib/lean/Init/Grind/CommRing.olean.private +lib/lean/Init/Grind/CommRing.olean.server +lib/lean/Init/Grind/CommRing/Basic.ilean +lib/lean/Init/Grind/CommRing/Basic.olean +lib/lean/Init/Grind/CommRing/Basic.olean.private +lib/lean/Init/Grind/CommRing/Basic.olean.server +lib/lean/Init/Grind/CommRing/BitVec.ilean +lib/lean/Init/Grind/CommRing/BitVec.olean +lib/lean/Init/Grind/CommRing/BitVec.olean.private +lib/lean/Init/Grind/CommRing/BitVec.olean.server +lib/lean/Init/Grind/CommRing/Int.ilean +lib/lean/Init/Grind/CommRing/Int.olean +lib/lean/Init/Grind/CommRing/Int.olean.private +lib/lean/Init/Grind/CommRing/Int.olean.server +lib/lean/Init/Grind/CommRing/Poly.ilean +lib/lean/Init/Grind/CommRing/Poly.olean +lib/lean/Init/Grind/CommRing/Poly.olean.private +lib/lean/Init/Grind/CommRing/Poly.olean.server +lib/lean/Init/Grind/CommRing/SInt.ilean +lib/lean/Init/Grind/CommRing/SInt.olean +lib/lean/Init/Grind/CommRing/SInt.olean.private +lib/lean/Init/Grind/CommRing/SInt.olean.server +lib/lean/Init/Grind/CommRing/UInt.ilean +lib/lean/Init/Grind/CommRing/UInt.olean +lib/lean/Init/Grind/CommRing/UInt.olean.private +lib/lean/Init/Grind/CommRing/UInt.olean.server +lib/lean/Init/Grind/Ext.ilean +lib/lean/Init/Grind/Ext.olean +lib/lean/Init/Grind/Ext.olean.private +lib/lean/Init/Grind/Ext.olean.server lib/lean/Init/Grind/Lemmas.ilean lib/lean/Init/Grind/Lemmas.olean +lib/lean/Init/Grind/Lemmas.olean.private +lib/lean/Init/Grind/Lemmas.olean.server lib/lean/Init/Grind/Norm.ilean lib/lean/Init/Grind/Norm.olean +lib/lean/Init/Grind/Norm.olean.private +lib/lean/Init/Grind/Norm.olean.server +lib/lean/Init/Grind/Offset.ilean +lib/lean/Init/Grind/Offset.olean +lib/lean/Init/Grind/Offset.olean.private +lib/lean/Init/Grind/Offset.olean.server +lib/lean/Init/Grind/PP.ilean +lib/lean/Init/Grind/PP.olean +lib/lean/Init/Grind/PP.olean.private +lib/lean/Init/Grind/PP.olean.server +lib/lean/Init/Grind/Propagator.ilean +lib/lean/Init/Grind/Propagator.olean +lib/lean/Init/Grind/Propagator.olean.private +lib/lean/Init/Grind/Propagator.olean.server lib/lean/Init/Grind/Tactics.ilean lib/lean/Init/Grind/Tactics.olean +lib/lean/Init/Grind/Tactics.olean.private +lib/lean/Init/Grind/Tactics.olean.server +lib/lean/Init/Grind/Util.ilean +lib/lean/Init/Grind/Util.olean +lib/lean/Init/Grind/Util.olean.private +lib/lean/Init/Grind/Util.olean.server lib/lean/Init/Guard.ilean lib/lean/Init/Guard.olean +lib/lean/Init/Guard.olean.private +lib/lean/Init/Guard.olean.server lib/lean/Init/Hints.ilean lib/lean/Init/Hints.olean +lib/lean/Init/Hints.olean.private +lib/lean/Init/Hints.olean.server +lib/lean/Init/Internal.ilean +lib/lean/Init/Internal.olean +lib/lean/Init/Internal.olean.private +lib/lean/Init/Internal.olean.server +lib/lean/Init/Internal/Order.ilean +lib/lean/Init/Internal/Order.olean +lib/lean/Init/Internal/Order.olean.private +lib/lean/Init/Internal/Order.olean.server +lib/lean/Init/Internal/Order/Basic.ilean +lib/lean/Init/Internal/Order/Basic.olean +lib/lean/Init/Internal/Order/Basic.olean.private +lib/lean/Init/Internal/Order/Basic.olean.server +lib/lean/Init/Internal/Order/Lemmas.ilean +lib/lean/Init/Internal/Order/Lemmas.olean +lib/lean/Init/Internal/Order/Lemmas.olean.private +lib/lean/Init/Internal/Order/Lemmas.olean.server +lib/lean/Init/Internal/Order/Tactic.ilean +lib/lean/Init/Internal/Order/Tactic.olean +lib/lean/Init/Internal/Order/Tactic.olean.private +lib/lean/Init/Internal/Order/Tactic.olean.server lib/lean/Init/MacroTrace.ilean lib/lean/Init/MacroTrace.olean +lib/lean/Init/MacroTrace.olean.private +lib/lean/Init/MacroTrace.olean.server lib/lean/Init/Meta.ilean lib/lean/Init/Meta.olean +lib/lean/Init/Meta.olean.private +lib/lean/Init/Meta.olean.server lib/lean/Init/MetaTypes.ilean lib/lean/Init/MetaTypes.olean +lib/lean/Init/MetaTypes.olean.private +lib/lean/Init/MetaTypes.olean.server lib/lean/Init/Notation.ilean lib/lean/Init/Notation.olean +lib/lean/Init/Notation.olean.private +lib/lean/Init/Notation.olean.server lib/lean/Init/NotationExtra.ilean lib/lean/Init/NotationExtra.olean +lib/lean/Init/NotationExtra.olean.private +lib/lean/Init/NotationExtra.olean.server lib/lean/Init/Omega.ilean lib/lean/Init/Omega.olean +lib/lean/Init/Omega.olean.private +lib/lean/Init/Omega.olean.server lib/lean/Init/Omega/Coeffs.ilean lib/lean/Init/Omega/Coeffs.olean +lib/lean/Init/Omega/Coeffs.olean.private +lib/lean/Init/Omega/Coeffs.olean.server lib/lean/Init/Omega/Constraint.ilean lib/lean/Init/Omega/Constraint.olean +lib/lean/Init/Omega/Constraint.olean.private +lib/lean/Init/Omega/Constraint.olean.server lib/lean/Init/Omega/Int.ilean lib/lean/Init/Omega/Int.olean +lib/lean/Init/Omega/Int.olean.private +lib/lean/Init/Omega/Int.olean.server lib/lean/Init/Omega/IntList.ilean lib/lean/Init/Omega/IntList.olean +lib/lean/Init/Omega/IntList.olean.private +lib/lean/Init/Omega/IntList.olean.server lib/lean/Init/Omega/LinearCombo.ilean lib/lean/Init/Omega/LinearCombo.olean +lib/lean/Init/Omega/LinearCombo.olean.private +lib/lean/Init/Omega/LinearCombo.olean.server lib/lean/Init/Omega/Logic.ilean lib/lean/Init/Omega/Logic.olean +lib/lean/Init/Omega/Logic.olean.private +lib/lean/Init/Omega/Logic.olean.server lib/lean/Init/Prelude.ilean lib/lean/Init/Prelude.olean +lib/lean/Init/Prelude.olean.private +lib/lean/Init/Prelude.olean.server lib/lean/Init/PropLemmas.ilean lib/lean/Init/PropLemmas.olean +lib/lean/Init/PropLemmas.olean.private +lib/lean/Init/PropLemmas.olean.server lib/lean/Init/RCases.ilean lib/lean/Init/RCases.olean +lib/lean/Init/RCases.olean.private +lib/lean/Init/RCases.olean.server lib/lean/Init/ShareCommon.ilean lib/lean/Init/ShareCommon.olean +lib/lean/Init/ShareCommon.olean.private +lib/lean/Init/ShareCommon.olean.server lib/lean/Init/SimpLemmas.ilean lib/lean/Init/SimpLemmas.olean +lib/lean/Init/SimpLemmas.olean.private +lib/lean/Init/SimpLemmas.olean.server lib/lean/Init/Simproc.ilean lib/lean/Init/Simproc.olean +lib/lean/Init/Simproc.olean.private +lib/lean/Init/Simproc.olean.server lib/lean/Init/SizeOf.ilean lib/lean/Init/SizeOf.olean +lib/lean/Init/SizeOf.olean.private +lib/lean/Init/SizeOf.olean.server lib/lean/Init/SizeOfLemmas.ilean lib/lean/Init/SizeOfLemmas.olean +lib/lean/Init/SizeOfLemmas.olean.private +lib/lean/Init/SizeOfLemmas.olean.server +lib/lean/Init/Syntax.ilean +lib/lean/Init/Syntax.olean +lib/lean/Init/Syntax.olean.private +lib/lean/Init/Syntax.olean.server lib/lean/Init/System.ilean lib/lean/Init/System.olean +lib/lean/Init/System.olean.private +lib/lean/Init/System.olean.server lib/lean/Init/System/FilePath.ilean lib/lean/Init/System/FilePath.olean +lib/lean/Init/System/FilePath.olean.private +lib/lean/Init/System/FilePath.olean.server lib/lean/Init/System/IO.ilean lib/lean/Init/System/IO.olean +lib/lean/Init/System/IO.olean.private +lib/lean/Init/System/IO.olean.server lib/lean/Init/System/IOError.ilean lib/lean/Init/System/IOError.olean +lib/lean/Init/System/IOError.olean.private +lib/lean/Init/System/IOError.olean.server lib/lean/Init/System/Mutex.ilean lib/lean/Init/System/Mutex.olean +lib/lean/Init/System/Mutex.olean.private +lib/lean/Init/System/Mutex.olean.server lib/lean/Init/System/Platform.ilean lib/lean/Init/System/Platform.olean +lib/lean/Init/System/Platform.olean.private +lib/lean/Init/System/Platform.olean.server lib/lean/Init/System/Promise.ilean lib/lean/Init/System/Promise.olean +lib/lean/Init/System/Promise.olean.private +lib/lean/Init/System/Promise.olean.server lib/lean/Init/System/ST.ilean lib/lean/Init/System/ST.olean +lib/lean/Init/System/ST.olean.private +lib/lean/Init/System/ST.olean.server lib/lean/Init/System/Uri.ilean lib/lean/Init/System/Uri.olean +lib/lean/Init/System/Uri.olean.private +lib/lean/Init/System/Uri.olean.server lib/lean/Init/Tactics.ilean lib/lean/Init/Tactics.olean +lib/lean/Init/Tactics.olean.private +lib/lean/Init/Tactics.olean.server lib/lean/Init/TacticsExtra.ilean lib/lean/Init/TacticsExtra.olean +lib/lean/Init/TacticsExtra.olean.private +lib/lean/Init/TacticsExtra.olean.server +lib/lean/Init/Task.ilean +lib/lean/Init/Task.olean +lib/lean/Init/Task.olean.private +lib/lean/Init/Task.olean.server +lib/lean/Init/Try.ilean +lib/lean/Init/Try.olean +lib/lean/Init/Try.olean.private +lib/lean/Init/Try.olean.server lib/lean/Init/Util.ilean lib/lean/Init/Util.olean +lib/lean/Init/Util.olean.private +lib/lean/Init/Util.olean.server lib/lean/Init/WF.ilean lib/lean/Init/WF.olean +lib/lean/Init/WF.olean.private +lib/lean/Init/WF.olean.server lib/lean/Init/WFTactics.ilean lib/lean/Init/WFTactics.olean +lib/lean/Init/WFTactics.olean.private +lib/lean/Init/WFTactics.olean.server +lib/lean/Init/While.ilean +lib/lean/Init/While.olean +lib/lean/Init/While.olean.private +lib/lean/Init/While.olean.server lib/lean/Lake.ilean lib/lean/Lake.olean lib/lean/Lake/Build.ilean lib/lean/Lake/Build.olean lib/lean/Lake/Build/Actions.ilean lib/lean/Lake/Build/Actions.olean -lib/lean/Lake/Build/Basic.ilean -lib/lean/Lake/Build/Basic.olean lib/lean/Lake/Build/Common.ilean lib/lean/Lake/Build/Common.olean +lib/lean/Lake/Build/Context.ilean +lib/lean/Lake/Build/Context.olean lib/lean/Lake/Build/Data.ilean lib/lean/Lake/Build/Data.olean lib/lean/Lake/Build/Executable.ilean lib/lean/Lake/Build/Executable.olean +lib/lean/Lake/Build/ExternLib.ilean +lib/lean/Lake/Build/ExternLib.olean lib/lean/Lake/Build/Facets.ilean lib/lean/Lake/Build/Facets.olean lib/lean/Lake/Build/Fetch.ilean @@ -429,8 +1241,18 @@ lib/lean/Lake/Build/Index.ilean lib/lean/Lake/Build/Index.olean lib/lean/Lake/Build/Info.ilean lib/lean/Lake/Build/Info.olean +lib/lean/Lake/Build/InitFacets.ilean +lib/lean/Lake/Build/InitFacets.olean +lib/lean/Lake/Build/InputFile.ilean +lib/lean/Lake/Build/InputFile.olean lib/lean/Lake/Build/Job.ilean lib/lean/Lake/Build/Job.olean +lib/lean/Lake/Build/Job/Basic.ilean +lib/lean/Lake/Build/Job/Basic.olean +lib/lean/Lake/Build/Job/Monad.ilean +lib/lean/Lake/Build/Job/Monad.olean +lib/lean/Lake/Build/Job/Register.ilean +lib/lean/Lake/Build/Job/Register.olean lib/lean/Lake/Build/Key.ilean lib/lean/Lake/Build/Key.olean lib/lean/Lake/Build/Library.ilean @@ -443,6 +1265,12 @@ lib/lean/Lake/Build/Run.ilean lib/lean/Lake/Build/Run.olean lib/lean/Lake/Build/Store.ilean lib/lean/Lake/Build/Store.olean +lib/lean/Lake/Build/Target.ilean +lib/lean/Lake/Build/Target.olean +lib/lean/Lake/Build/Target/Basic.ilean +lib/lean/Lake/Build/Target/Basic.olean +lib/lean/Lake/Build/Target/Fetch.ilean +lib/lean/Lake/Build/Target/Fetch.olean lib/lean/Lake/Build/Targets.ilean lib/lean/Lake/Build/Targets.olean lib/lean/Lake/Build/Topological.ilean @@ -473,12 +1301,18 @@ lib/lean/Lake/CLI/Translate/Toml.ilean lib/lean/Lake/CLI/Translate/Toml.olean lib/lean/Lake/Config.ilean lib/lean/Lake/Config.olean +lib/lean/Lake/Config/ConfigDecl.ilean +lib/lean/Lake/Config/ConfigDecl.olean +lib/lean/Lake/Config/ConfigTarget.ilean +lib/lean/Lake/Config/ConfigTarget.olean lib/lean/Lake/Config/Context.ilean lib/lean/Lake/Config/Context.olean lib/lean/Lake/Config/Defaults.ilean lib/lean/Lake/Config/Defaults.olean lib/lean/Lake/Config/Dependency.ilean lib/lean/Lake/Config/Dependency.olean +lib/lean/Lake/Config/Dynlib.ilean +lib/lean/Lake/Config/Dynlib.olean lib/lean/Lake/Config/Env.ilean lib/lean/Lake/Config/Env.olean lib/lean/Lake/Config/ExternLib.ilean @@ -489,8 +1323,14 @@ lib/lean/Lake/Config/FacetConfig.ilean lib/lean/Lake/Config/FacetConfig.olean lib/lean/Lake/Config/Glob.ilean lib/lean/Lake/Config/Glob.olean +lib/lean/Lake/Config/InputFile.ilean +lib/lean/Lake/Config/InputFile.olean +lib/lean/Lake/Config/InputFileConfig.ilean +lib/lean/Lake/Config/InputFileConfig.olean lib/lean/Lake/Config/InstallPath.ilean lib/lean/Lake/Config/InstallPath.olean +lib/lean/Lake/Config/Kinds.ilean +lib/lean/Lake/Config/Kinds.olean lib/lean/Lake/Config/Lang.ilean lib/lean/Lake/Config/Lang.olean lib/lean/Lake/Config/LeanConfig.ilean @@ -503,14 +1343,20 @@ lib/lean/Lake/Config/LeanLib.ilean lib/lean/Lake/Config/LeanLib.olean lib/lean/Lake/Config/LeanLibConfig.ilean lib/lean/Lake/Config/LeanLibConfig.olean +lib/lean/Lake/Config/Meta.ilean +lib/lean/Lake/Config/Meta.olean lib/lean/Lake/Config/Module.ilean lib/lean/Lake/Config/Module.olean lib/lean/Lake/Config/Monad.ilean lib/lean/Lake/Config/Monad.olean lib/lean/Lake/Config/Opaque.ilean lib/lean/Lake/Config/Opaque.olean +lib/lean/Lake/Config/OutFormat.ilean +lib/lean/Lake/Config/OutFormat.olean lib/lean/Lake/Config/Package.ilean lib/lean/Lake/Config/Package.olean +lib/lean/Lake/Config/Pattern.ilean +lib/lean/Lake/Config/Pattern.olean lib/lean/Lake/Config/Script.ilean lib/lean/Lake/Config/Script.olean lib/lean/Lake/Config/TargetConfig.ilean @@ -531,6 +1377,8 @@ lib/lean/Lake/DSL/DeclUtil.ilean lib/lean/Lake/DSL/DeclUtil.olean lib/lean/Lake/DSL/Extensions.ilean lib/lean/Lake/DSL/Extensions.olean +lib/lean/Lake/DSL/Key.ilean +lib/lean/Lake/DSL/Key.olean lib/lean/Lake/DSL/Meta.ilean lib/lean/Lake/DSL/Meta.olean lib/lean/Lake/DSL/Package.ilean @@ -539,8 +1387,12 @@ lib/lean/Lake/DSL/Require.ilean lib/lean/Lake/DSL/Require.olean lib/lean/Lake/DSL/Script.ilean lib/lean/Lake/DSL/Script.olean +lib/lean/Lake/DSL/Syntax.ilean +lib/lean/Lake/DSL/Syntax.olean lib/lean/Lake/DSL/Targets.ilean lib/lean/Lake/DSL/Targets.olean +lib/lean/Lake/DSL/VerLit.ilean +lib/lean/Lake/DSL/VerLit.olean lib/lean/Lake/Load.ilean lib/lean/Lake/Load.olean lib/lean/Lake/Load/Config.ilean @@ -563,8 +1415,6 @@ lib/lean/Lake/Load/Toml.ilean lib/lean/Lake/Load/Toml.olean lib/lean/Lake/Load/Workspace.ilean lib/lean/Lake/Load/Workspace.olean -lib/lean/Lake/Main.ilean -lib/lean/Lake/Main.olean lib/lean/Lake/Reservoir.ilean lib/lean/Lake/Reservoir.olean lib/lean/Lake/Toml.ilean @@ -605,6 +1455,8 @@ lib/lean/Lake/Util/Cycle.ilean lib/lean/Lake/Util/Cycle.olean lib/lean/Lake/Util/DRBMap.ilean lib/lean/Lake/Util/DRBMap.olean +lib/lean/Lake/Util/Date.ilean +lib/lean/Lake/Util/Date.olean lib/lean/Lake/Util/EStateT.ilean lib/lean/Lake/Util/EStateT.olean lib/lean/Lake/Util/EquipT.ilean @@ -641,6 +1493,8 @@ lib/lean/Lake/Util/NativeLib.ilean lib/lean/Lake/Util/NativeLib.olean lib/lean/Lake/Util/Opaque.ilean lib/lean/Lake/Util/Opaque.olean +lib/lean/Lake/Util/OpaqueType.ilean +lib/lean/Lake/Util/OpaqueType.olean lib/lean/Lake/Util/OrdHashSet.ilean lib/lean/Lake/Util/OrdHashSet.olean lib/lean/Lake/Util/OrderedTagAttribute.ilean @@ -661,6 +1515,8 @@ lib/lean/Lake/Util/Version.ilean lib/lean/Lake/Util/Version.olean lib/lean/Lake/Version.ilean lib/lean/Lake/Version.olean +lib/lean/LakeMain.ilean +lib/lean/LakeMain.olean lib/lean/Lean.ilean lib/lean/Lean.olean lib/lean/Lean/AddDecl.ilean @@ -783,8 +1639,6 @@ lib/lean/Lean/Compiler/LCNF/FixedParams.ilean lib/lean/Lean/Compiler/LCNF/FixedParams.olean lib/lean/Lean/Compiler/LCNF/FloatLetIn.ilean lib/lean/Lean/Compiler/LCNF/FloatLetIn.olean -lib/lean/Lean/Compiler/LCNF/ForEachExpr.ilean -lib/lean/Lean/Compiler/LCNF/ForEachExpr.olean lib/lean/Lean/Compiler/LCNF/InferType.ilean lib/lean/Lean/Compiler/LCNF/InferType.olean lib/lean/Lean/Compiler/LCNF/Internalize.ilean @@ -895,14 +1749,12 @@ lib/lean/Lean/Data/Array.ilean lib/lean/Lean/Data/Array.olean lib/lean/Lean/Data/AssocList.ilean lib/lean/Lean/Data/AssocList.olean +lib/lean/Lean/Data/DeclarationRange.ilean +lib/lean/Lean/Data/DeclarationRange.olean lib/lean/Lean/Data/Format.ilean lib/lean/Lean/Data/Format.olean lib/lean/Lean/Data/FuzzyMatching.ilean lib/lean/Lean/Data/FuzzyMatching.olean -lib/lean/Lean/Data/HashMap.ilean -lib/lean/Lean/Data/HashMap.olean -lib/lean/Lean/Data/HashSet.ilean -lib/lean/Lean/Data/HashSet.olean lib/lean/Lean/Data/Json.ilean lib/lean/Lean/Data/Json.olean lib/lean/Lean/Data/Json/Basic.ilean @@ -929,6 +1781,8 @@ lib/lean/Lean/Data/Lsp.ilean lib/lean/Lean/Data/Lsp.olean lib/lean/Lean/Data/Lsp/Basic.ilean lib/lean/Lean/Data/Lsp/Basic.olean +lib/lean/Lean/Data/Lsp/CancelParams.ilean +lib/lean/Lean/Data/Lsp/CancelParams.olean lib/lean/Lean/Data/Lsp/Capabilities.ilean lib/lean/Lean/Data/Lsp/Capabilities.olean lib/lean/Lean/Data/Lsp/Client.ilean @@ -977,12 +1831,12 @@ lib/lean/Lean/Data/Position.ilean lib/lean/Lean/Data/Position.olean lib/lean/Lean/Data/PrefixTree.ilean lib/lean/Lean/Data/PrefixTree.olean +lib/lean/Lean/Data/RArray.ilean +lib/lean/Lean/Data/RArray.olean lib/lean/Lean/Data/RBMap.ilean lib/lean/Lean/Data/RBMap.olean lib/lean/Lean/Data/RBTree.ilean lib/lean/Lean/Data/RBTree.olean -lib/lean/Lean/Data/Rat.ilean -lib/lean/Lean/Data/Rat.olean lib/lean/Lean/Data/SMap.ilean lib/lean/Lean/Data/SMap.olean lib/lean/Lean/Data/SSet.ilean @@ -1001,8 +1855,12 @@ lib/lean/Lean/DeclarationRange.ilean lib/lean/Lean/DeclarationRange.olean lib/lean/Lean/DocString.ilean lib/lean/Lean/DocString.olean +lib/lean/Lean/DocString/Add.ilean +lib/lean/Lean/DocString/Add.olean lib/lean/Lean/DocString/Extension.ilean lib/lean/Lean/DocString/Extension.olean +lib/lean/Lean/DocString/Links.ilean +lib/lean/Lean/DocString/Links.olean lib/lean/Lean/Elab.ilean lib/lean/Lean/Elab.olean lib/lean/Lean/Elab/App.ilean @@ -1023,6 +1881,8 @@ lib/lean/Lean/Elab/BindersUtil.ilean lib/lean/Lean/Elab/BindersUtil.olean lib/lean/Lean/Elab/BuiltinCommand.ilean lib/lean/Lean/Elab/BuiltinCommand.olean +lib/lean/Lean/Elab/BuiltinEvalCommand.ilean +lib/lean/Lean/Elab/BuiltinEvalCommand.olean lib/lean/Lean/Elab/BuiltinNotation.ilean lib/lean/Lean/Elab/BuiltinNotation.olean lib/lean/Lean/Elab/BuiltinTerm.ilean @@ -1071,6 +1931,8 @@ lib/lean/Lean/Elab/Deriving/Repr.ilean lib/lean/Lean/Elab/Deriving/Repr.olean lib/lean/Lean/Elab/Deriving/SizeOf.ilean lib/lean/Lean/Elab/Deriving/SizeOf.olean +lib/lean/Lean/Elab/Deriving/ToExpr.ilean +lib/lean/Lean/Elab/Deriving/ToExpr.olean lib/lean/Lean/Elab/Deriving/TypeName.ilean lib/lean/Lean/Elab/Deriving/TypeName.olean lib/lean/Lean/Elab/Deriving/Util.ilean @@ -1097,10 +1959,14 @@ lib/lean/Lean/Elab/Inductive.ilean lib/lean/Lean/Elab/Inductive.olean lib/lean/Lean/Elab/InfoTree.ilean lib/lean/Lean/Elab/InfoTree.olean +lib/lean/Lean/Elab/InfoTree/InlayHints.ilean +lib/lean/Lean/Elab/InfoTree/InlayHints.olean lib/lean/Lean/Elab/InfoTree/Main.ilean lib/lean/Lean/Elab/InfoTree/Main.olean lib/lean/Lean/Elab/InfoTree/Types.ilean lib/lean/Lean/Elab/InfoTree/Types.olean +lib/lean/Lean/Elab/InfoTrees.ilean +lib/lean/Lean/Elab/InfoTrees.olean lib/lean/Lean/Elab/InheritDoc.ilean lib/lean/Lean/Elab/InheritDoc.olean lib/lean/Lean/Elab/LetRec.ilean @@ -1123,6 +1989,8 @@ lib/lean/Lean/Elab/Mixfix.ilean lib/lean/Lean/Elab/Mixfix.olean lib/lean/Lean/Elab/MutualDef.ilean lib/lean/Lean/Elab/MutualDef.olean +lib/lean/Lean/Elab/MutualInductive.ilean +lib/lean/Lean/Elab/MutualInductive.olean lib/lean/Lean/Elab/Notation.ilean lib/lean/Lean/Elab/Notation.olean lib/lean/Lean/Elab/Open.ilean @@ -1139,12 +2007,24 @@ lib/lean/Lean/Elab/PreDefinition/EqUnfold.ilean lib/lean/Lean/Elab/PreDefinition/EqUnfold.olean lib/lean/Lean/Elab/PreDefinition/Eqns.ilean lib/lean/Lean/Elab/PreDefinition/Eqns.olean +lib/lean/Lean/Elab/PreDefinition/FixedParams.ilean +lib/lean/Lean/Elab/PreDefinition/FixedParams.olean lib/lean/Lean/Elab/PreDefinition/Main.ilean lib/lean/Lean/Elab/PreDefinition/Main.olean lib/lean/Lean/Elab/PreDefinition/MkInhabitant.ilean lib/lean/Lean/Elab/PreDefinition/MkInhabitant.olean +lib/lean/Lean/Elab/PreDefinition/Mutual.ilean +lib/lean/Lean/Elab/PreDefinition/Mutual.olean lib/lean/Lean/Elab/PreDefinition/Nonrec/Eqns.ilean lib/lean/Lean/Elab/PreDefinition/Nonrec/Eqns.olean +lib/lean/Lean/Elab/PreDefinition/PartialFixpoint.ilean +lib/lean/Lean/Elab/PreDefinition/PartialFixpoint.olean +lib/lean/Lean/Elab/PreDefinition/PartialFixpoint/Eqns.ilean +lib/lean/Lean/Elab/PreDefinition/PartialFixpoint/Eqns.olean +lib/lean/Lean/Elab/PreDefinition/PartialFixpoint/Induction.ilean +lib/lean/Lean/Elab/PreDefinition/PartialFixpoint/Induction.olean +lib/lean/Lean/Elab/PreDefinition/PartialFixpoint/Main.ilean +lib/lean/Lean/Elab/PreDefinition/PartialFixpoint/Main.olean lib/lean/Lean/Elab/PreDefinition/Structural.ilean lib/lean/Lean/Elab/PreDefinition/Structural.olean lib/lean/Lean/Elab/PreDefinition/Structural/BRecOn.ilean @@ -1167,10 +2047,10 @@ lib/lean/Lean/Elab/PreDefinition/Structural/RecArgInfo.ilean lib/lean/Lean/Elab/PreDefinition/Structural/RecArgInfo.olean lib/lean/Lean/Elab/PreDefinition/Structural/SmartUnfolding.ilean lib/lean/Lean/Elab/PreDefinition/Structural/SmartUnfolding.olean -lib/lean/Lean/Elab/PreDefinition/TerminationArgument.ilean -lib/lean/Lean/Elab/PreDefinition/TerminationArgument.olean lib/lean/Lean/Elab/PreDefinition/TerminationHint.ilean lib/lean/Lean/Elab/PreDefinition/TerminationHint.olean +lib/lean/Lean/Elab/PreDefinition/TerminationMeasure.ilean +lib/lean/Lean/Elab/PreDefinition/TerminationMeasure.olean lib/lean/Lean/Elab/PreDefinition/WF.ilean lib/lean/Lean/Elab/PreDefinition/WF.olean lib/lean/Lean/Elab/PreDefinition/WF/Basic.ilean @@ -1179,10 +2059,10 @@ lib/lean/Lean/Elab/PreDefinition/WF/Eqns.ilean lib/lean/Lean/Elab/PreDefinition/WF/Eqns.olean lib/lean/Lean/Elab/PreDefinition/WF/Fix.ilean lib/lean/Lean/Elab/PreDefinition/WF/Fix.olean +lib/lean/Lean/Elab/PreDefinition/WF/FloatRecApp.ilean +lib/lean/Lean/Elab/PreDefinition/WF/FloatRecApp.olean lib/lean/Lean/Elab/PreDefinition/WF/GuessLex.ilean lib/lean/Lean/Elab/PreDefinition/WF/GuessLex.olean -lib/lean/Lean/Elab/PreDefinition/WF/Ite.ilean -lib/lean/Lean/Elab/PreDefinition/WF/Ite.olean lib/lean/Lean/Elab/PreDefinition/WF/Main.ilean lib/lean/Lean/Elab/PreDefinition/WF/Main.olean lib/lean/Lean/Elab/PreDefinition/WF/PackMutual.ilean @@ -1191,6 +2071,8 @@ lib/lean/Lean/Elab/PreDefinition/WF/Preprocess.ilean lib/lean/Lean/Elab/PreDefinition/WF/Preprocess.olean lib/lean/Lean/Elab/PreDefinition/WF/Rel.ilean lib/lean/Lean/Elab/PreDefinition/WF/Rel.olean +lib/lean/Lean/Elab/PreDefinition/WF/Unfold.ilean +lib/lean/Lean/Elab/PreDefinition/WF/Unfold.olean lib/lean/Lean/Elab/Print.ilean lib/lean/Lean/Elab/Print.olean lib/lean/Lean/Elab/Quotation.ilean @@ -1201,6 +2083,8 @@ lib/lean/Lean/Elab/Quotation/Util.ilean lib/lean/Lean/Elab/Quotation/Util.olean lib/lean/Lean/Elab/RecAppSyntax.ilean lib/lean/Lean/Elab/RecAppSyntax.olean +lib/lean/Lean/Elab/RecommendedSpelling.ilean +lib/lean/Lean/Elab/RecommendedSpelling.olean lib/lean/Lean/Elab/SetOption.ilean lib/lean/Lean/Elab/SetOption.olean lib/lean/Lean/Elab/StructInst.ilean @@ -1213,6 +2097,8 @@ lib/lean/Lean/Elab/SyntheticMVars.ilean lib/lean/Lean/Elab/SyntheticMVars.olean lib/lean/Lean/Elab/Tactic.ilean lib/lean/Lean/Elab/Tactic.olean +lib/lean/Lean/Elab/Tactic/AsAuxLemma.ilean +lib/lean/Lean/Elab/Tactic/AsAuxLemma.olean lib/lean/Lean/Elab/Tactic/BVDecide.ilean lib/lean/Lean/Elab/Tactic/BVDecide.olean lib/lean/Lean/Elab/Tactic/BVDecide/External.ilean @@ -1233,6 +2119,10 @@ lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVLogical.ilean lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVLogical.olean lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVPred.ilean lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVPred.olean +lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedLemmas.ilean +lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedLemmas.olean +lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reify.ilean +lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reify.olean lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/SatAtBVLogical.ilean lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/SatAtBVLogical.olean lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/BVTrace.ilean @@ -1241,6 +2131,30 @@ lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/LRAT.ilean lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/LRAT.olean lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/Normalize.ilean lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/Normalize.olean +lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/AC.ilean +lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/AC.olean +lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/AndFlatten.ilean +lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/AndFlatten.olean +lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/ApplyControlFlow.ilean +lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/ApplyControlFlow.olean +lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Basic.ilean +lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Basic.olean +lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/EmbeddedConstraint.ilean +lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/EmbeddedConstraint.olean +lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Enums.ilean +lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Enums.olean +lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/IntToBitVec.ilean +lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/IntToBitVec.olean +lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Rewrite.ilean +lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Rewrite.olean +lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/ShortCircuit.ilean +lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/ShortCircuit.olean +lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Simproc.ilean +lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Simproc.olean +lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Structures.ilean +lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Structures.olean +lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/TypeAnalysis.ilean +lib/lean/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/TypeAnalysis.olean lib/lean/Lean/Elab/Tactic/BVDecide/LRAT.ilean lib/lean/Lean/Elab/Tactic/BVDecide/LRAT.olean lib/lean/Lean/Elab/Tactic/BVDecide/LRAT/Trim.ilean @@ -1251,12 +2165,12 @@ lib/lean/Lean/Elab/Tactic/BoolToPropSimps.ilean lib/lean/Lean/Elab/Tactic/BoolToPropSimps.olean lib/lean/Lean/Elab/Tactic/BuiltinTactic.ilean lib/lean/Lean/Elab/Tactic/BuiltinTactic.olean -lib/lean/Lean/Elab/Tactic/Cache.ilean -lib/lean/Lean/Elab/Tactic/Cache.olean lib/lean/Lean/Elab/Tactic/Calc.ilean lib/lean/Lean/Elab/Tactic/Calc.olean lib/lean/Lean/Elab/Tactic/Change.ilean lib/lean/Lean/Elab/Tactic/Change.olean +lib/lean/Lean/Elab/Tactic/Classical.ilean +lib/lean/Lean/Elab/Tactic/Classical.olean lib/lean/Lean/Elab/Tactic/Config.ilean lib/lean/Lean/Elab/Tactic/Config.olean lib/lean/Lean/Elab/Tactic/Congr.ilean @@ -1271,6 +2185,8 @@ lib/lean/Lean/Elab/Tactic/Conv/Congr.ilean lib/lean/Lean/Elab/Tactic/Conv/Congr.olean lib/lean/Lean/Elab/Tactic/Conv/Delta.ilean lib/lean/Lean/Elab/Tactic/Conv/Delta.olean +lib/lean/Lean/Elab/Tactic/Conv/Lets.ilean +lib/lean/Lean/Elab/Tactic/Conv/Lets.olean lib/lean/Lean/Elab/Tactic/Conv/Pattern.ilean lib/lean/Lean/Elab/Tactic/Conv/Pattern.olean lib/lean/Lean/Elab/Tactic/Conv/Rewrite.ilean @@ -1287,18 +2203,24 @@ lib/lean/Lean/Elab/Tactic/Doc.ilean lib/lean/Lean/Elab/Tactic/Doc.olean lib/lean/Lean/Elab/Tactic/ElabTerm.ilean lib/lean/Lean/Elab/Tactic/ElabTerm.olean +lib/lean/Lean/Elab/Tactic/ExposeNames.ilean +lib/lean/Lean/Elab/Tactic/ExposeNames.olean lib/lean/Lean/Elab/Tactic/Ext.ilean lib/lean/Lean/Elab/Tactic/Ext.olean lib/lean/Lean/Elab/Tactic/FalseOrByContra.ilean lib/lean/Lean/Elab/Tactic/FalseOrByContra.olean lib/lean/Lean/Elab/Tactic/Generalize.ilean lib/lean/Lean/Elab/Tactic/Generalize.olean +lib/lean/Lean/Elab/Tactic/Grind.ilean +lib/lean/Lean/Elab/Tactic/Grind.olean lib/lean/Lean/Elab/Tactic/Guard.ilean lib/lean/Lean/Elab/Tactic/Guard.olean lib/lean/Lean/Elab/Tactic/Induction.ilean lib/lean/Lean/Elab/Tactic/Induction.olean lib/lean/Lean/Elab/Tactic/Injection.ilean lib/lean/Lean/Elab/Tactic/Injection.olean +lib/lean/Lean/Elab/Tactic/Lets.ilean +lib/lean/Lean/Elab/Tactic/Lets.olean lib/lean/Lean/Elab/Tactic/LibrarySearch.ilean lib/lean/Lean/Elab/Tactic/LibrarySearch.olean lib/lean/Lean/Elab/Tactic/Location.ilean @@ -1307,6 +2229,8 @@ lib/lean/Lean/Elab/Tactic/Match.ilean lib/lean/Lean/Elab/Tactic/Match.olean lib/lean/Lean/Elab/Tactic/Meta.ilean lib/lean/Lean/Elab/Tactic/Meta.olean +lib/lean/Lean/Elab/Tactic/Monotonicity.ilean +lib/lean/Lean/Elab/Tactic/Monotonicity.olean lib/lean/Lean/Elab/Tactic/NormCast.ilean lib/lean/Lean/Elab/Tactic/NormCast.olean lib/lean/Lean/Elab/Tactic/Omega.ilean @@ -1333,6 +2257,8 @@ lib/lean/Lean/Elab/Tactic/ShowTerm.ilean lib/lean/Lean/Elab/Tactic/ShowTerm.olean lib/lean/Lean/Elab/Tactic/Simp.ilean lib/lean/Lean/Elab/Tactic/Simp.olean +lib/lean/Lean/Elab/Tactic/SimpArith.ilean +lib/lean/Lean/Elab/Tactic/SimpArith.olean lib/lean/Lean/Elab/Tactic/SimpTrace.ilean lib/lean/Lean/Elab/Tactic/SimpTrace.olean lib/lean/Lean/Elab/Tactic/Simpa.ilean @@ -1345,6 +2271,10 @@ lib/lean/Lean/Elab/Tactic/Split.ilean lib/lean/Lean/Elab/Tactic/Split.olean lib/lean/Lean/Elab/Tactic/Symm.ilean lib/lean/Lean/Elab/Tactic/Symm.olean +lib/lean/Lean/Elab/Tactic/TreeTacAttr.ilean +lib/lean/Lean/Elab/Tactic/TreeTacAttr.olean +lib/lean/Lean/Elab/Tactic/Try.ilean +lib/lean/Lean/Elab/Tactic/Try.olean lib/lean/Lean/Elab/Tactic/Unfold.ilean lib/lean/Lean/Elab/Tactic/Unfold.olean lib/lean/Lean/Elab/Term.ilean @@ -1353,10 +2283,10 @@ lib/lean/Lean/Elab/Time.ilean lib/lean/Lean/Elab/Time.olean lib/lean/Lean/Elab/Util.ilean lib/lean/Lean/Elab/Util.olean +lib/lean/Lean/EnvExtension.ilean +lib/lean/Lean/EnvExtension.olean lib/lean/Lean/Environment.ilean lib/lean/Lean/Environment.olean -lib/lean/Lean/Eval.ilean -lib/lean/Lean/Eval.olean lib/lean/Lean/Exception.ilean lib/lean/Lean/Exception.olean lib/lean/Lean/Expr.ilean @@ -1379,8 +2309,8 @@ lib/lean/Lean/Language/Lean.ilean lib/lean/Lean/Language/Lean.olean lib/lean/Lean/Language/Lean/Types.ilean lib/lean/Lean/Language/Lean/Types.olean -lib/lean/Lean/LazyInitExtension.ilean -lib/lean/Lean/LazyInitExtension.olean +lib/lean/Lean/Language/Util.ilean +lib/lean/Lean/Language/Util.olean lib/lean/Lean/Level.ilean lib/lean/Lean/Level.olean lib/lean/Lean/Linter.ilean @@ -1393,6 +2323,8 @@ lib/lean/Lean/Linter/ConstructorAsVariable.ilean lib/lean/Lean/Linter/ConstructorAsVariable.olean lib/lean/Lean/Linter/Deprecated.ilean lib/lean/Lean/Linter/Deprecated.olean +lib/lean/Lean/Linter/List.ilean +lib/lean/Lean/Linter/List.olean lib/lean/Lean/Linter/MissingDocs.ilean lib/lean/Lean/Linter/MissingDocs.olean lib/lean/Lean/Linter/Omit.ilean @@ -1425,6 +2357,8 @@ lib/lean/Lean/Meta/ArgsPacker/Basic.ilean lib/lean/Lean/Meta/ArgsPacker/Basic.olean lib/lean/Lean/Meta/Basic.ilean lib/lean/Lean/Meta/Basic.olean +lib/lean/Lean/Meta/BinderNameHint.ilean +lib/lean/Lean/Meta/BinderNameHint.olean lib/lean/Lean/Meta/Canonicalizer.ilean lib/lean/Lean/Meta/Canonicalizer.olean lib/lean/Lean/Meta/Check.ilean @@ -1497,6 +2431,8 @@ lib/lean/Lean/Meta/Injective.ilean lib/lean/Lean/Meta/Injective.olean lib/lean/Lean/Meta/Instances.ilean lib/lean/Lean/Meta/Instances.olean +lib/lean/Lean/Meta/IntInstTesters.ilean +lib/lean/Lean/Meta/IntInstTesters.olean lib/lean/Lean/Meta/Iterator.ilean lib/lean/Lean/Meta/Iterator.olean lib/lean/Lean/Meta/KAbstract.ilean @@ -1543,6 +2479,8 @@ lib/lean/Lean/Meta/NatInstTesters.ilean lib/lean/Lean/Meta/NatInstTesters.olean lib/lean/Lean/Meta/Offset.ilean lib/lean/Lean/Meta/Offset.olean +lib/lean/Lean/Meta/Order.ilean +lib/lean/Lean/Meta/Order.olean lib/lean/Lean/Meta/PPGoal.ilean lib/lean/Lean/Meta/PPGoal.olean lib/lean/Lean/Meta/PProdN.ilean @@ -1555,6 +2493,8 @@ lib/lean/Lean/Meta/ReduceEval.ilean lib/lean/Lean/Meta/ReduceEval.olean lib/lean/Lean/Meta/SizeOf.ilean lib/lean/Lean/Meta/SizeOf.olean +lib/lean/Lean/Meta/Sorry.ilean +lib/lean/Lean/Meta/Sorry.olean lib/lean/Lean/Meta/Structure.ilean lib/lean/Lean/Meta/Structure.olean lib/lean/Lean/Meta/SynthInstance.ilean @@ -1593,26 +2533,184 @@ lib/lean/Lean/Meta/Tactic/Delta.ilean lib/lean/Lean/Meta/Tactic/Delta.olean lib/lean/Lean/Meta/Tactic/ElimInfo.ilean lib/lean/Lean/Meta/Tactic/ElimInfo.olean +lib/lean/Lean/Meta/Tactic/ExposeNames.ilean +lib/lean/Lean/Meta/Tactic/ExposeNames.olean +lib/lean/Lean/Meta/Tactic/Ext.ilean +lib/lean/Lean/Meta/Tactic/Ext.olean lib/lean/Lean/Meta/Tactic/FVarSubst.ilean lib/lean/Lean/Meta/Tactic/FVarSubst.olean lib/lean/Lean/Meta/Tactic/FunInd.ilean lib/lean/Lean/Meta/Tactic/FunInd.olean +lib/lean/Lean/Meta/Tactic/FunIndCollect.ilean +lib/lean/Lean/Meta/Tactic/FunIndCollect.olean +lib/lean/Lean/Meta/Tactic/FunIndInfo.ilean +lib/lean/Lean/Meta/Tactic/FunIndInfo.olean lib/lean/Lean/Meta/Tactic/Generalize.ilean lib/lean/Lean/Meta/Tactic/Generalize.olean lib/lean/Lean/Meta/Tactic/Grind.ilean lib/lean/Lean/Meta/Tactic/Grind.olean +lib/lean/Lean/Meta/Tactic/Grind/Arith.ilean +lib/lean/Lean/Meta/Tactic/Grind/Arith.olean +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing.ilean +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing.olean +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/DenoteExpr.ilean +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/DenoteExpr.olean +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/EqCnstr.ilean +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/EqCnstr.olean +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Internalize.ilean +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Internalize.olean +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Inv.ilean +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Inv.olean +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Poly.ilean +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Poly.olean +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Proof.ilean +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Proof.olean +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Reify.ilean +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Reify.olean +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/RingId.ilean +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/RingId.olean +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/ToExpr.ilean +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/ToExpr.olean +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Types.ilean +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Types.olean +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Util.ilean +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Util.olean +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Var.ilean +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Var.olean +lib/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat.ilean +lib/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat.olean +lib/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/DvdCnstr.ilean +lib/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/DvdCnstr.olean +lib/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.ilean +lib/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.olean +lib/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/Foreign.ilean +lib/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/Foreign.olean +lib/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/Inv.ilean +lib/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/Inv.olean +lib/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/LeCnstr.ilean +lib/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/LeCnstr.olean +lib/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/MBTC.ilean +lib/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/MBTC.olean +lib/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/Model.ilean +lib/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/Model.olean +lib/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/Nat.ilean +lib/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/Nat.olean +lib/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/Norm.ilean +lib/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/Norm.olean +lib/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.ilean +lib/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.olean +lib/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/Search.ilean +lib/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/Search.olean +lib/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/SearchM.ilean +lib/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/SearchM.olean +lib/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/Types.ilean +lib/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/Types.olean +lib/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/Util.ilean +lib/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/Util.olean +lib/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/Var.ilean +lib/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/Var.olean +lib/lean/Lean/Meta/Tactic/Grind/Arith/Internalize.ilean +lib/lean/Lean/Meta/Tactic/Grind/Arith/Internalize.olean +lib/lean/Lean/Meta/Tactic/Grind/Arith/Inv.ilean +lib/lean/Lean/Meta/Tactic/Grind/Arith/Inv.olean +lib/lean/Lean/Meta/Tactic/Grind/Arith/Main.ilean +lib/lean/Lean/Meta/Tactic/Grind/Arith/Main.olean +lib/lean/Lean/Meta/Tactic/Grind/Arith/Model.ilean +lib/lean/Lean/Meta/Tactic/Grind/Arith/Model.olean +lib/lean/Lean/Meta/Tactic/Grind/Arith/Offset.ilean +lib/lean/Lean/Meta/Tactic/Grind/Arith/Offset.olean +lib/lean/Lean/Meta/Tactic/Grind/Arith/Offset/Main.ilean +lib/lean/Lean/Meta/Tactic/Grind/Arith/Offset/Main.olean +lib/lean/Lean/Meta/Tactic/Grind/Arith/Offset/Model.ilean +lib/lean/Lean/Meta/Tactic/Grind/Arith/Offset/Model.olean +lib/lean/Lean/Meta/Tactic/Grind/Arith/Offset/Proof.ilean +lib/lean/Lean/Meta/Tactic/Grind/Arith/Offset/Proof.olean +lib/lean/Lean/Meta/Tactic/Grind/Arith/Offset/Types.ilean +lib/lean/Lean/Meta/Tactic/Grind/Arith/Offset/Types.olean +lib/lean/Lean/Meta/Tactic/Grind/Arith/Offset/Util.ilean +lib/lean/Lean/Meta/Tactic/Grind/Arith/Offset/Util.olean +lib/lean/Lean/Meta/Tactic/Grind/Arith/ProofUtil.ilean +lib/lean/Lean/Meta/Tactic/Grind/Arith/ProofUtil.olean +lib/lean/Lean/Meta/Tactic/Grind/Arith/Types.ilean +lib/lean/Lean/Meta/Tactic/Grind/Arith/Types.olean +lib/lean/Lean/Meta/Tactic/Grind/Arith/Util.ilean +lib/lean/Lean/Meta/Tactic/Grind/Arith/Util.olean lib/lean/Lean/Meta/Tactic/Grind/Attr.ilean lib/lean/Lean/Meta/Tactic/Grind/Attr.olean +lib/lean/Lean/Meta/Tactic/Grind/Beta.ilean +lib/lean/Lean/Meta/Tactic/Grind/Beta.olean +lib/lean/Lean/Meta/Tactic/Grind/Canon.ilean +lib/lean/Lean/Meta/Tactic/Grind/Canon.olean lib/lean/Lean/Meta/Tactic/Grind/Cases.ilean lib/lean/Lean/Meta/Tactic/Grind/Cases.olean +lib/lean/Lean/Meta/Tactic/Grind/CasesMatch.ilean +lib/lean/Lean/Meta/Tactic/Grind/CasesMatch.olean +lib/lean/Lean/Meta/Tactic/Grind/Combinators.ilean +lib/lean/Lean/Meta/Tactic/Grind/Combinators.olean lib/lean/Lean/Meta/Tactic/Grind/Core.ilean lib/lean/Lean/Meta/Tactic/Grind/Core.olean +lib/lean/Lean/Meta/Tactic/Grind/Ctor.ilean +lib/lean/Lean/Meta/Tactic/Grind/Ctor.olean +lib/lean/Lean/Meta/Tactic/Grind/Diseq.ilean +lib/lean/Lean/Meta/Tactic/Grind/Diseq.olean +lib/lean/Lean/Meta/Tactic/Grind/EMatch.ilean +lib/lean/Lean/Meta/Tactic/Grind/EMatch.olean +lib/lean/Lean/Meta/Tactic/Grind/EMatchTheorem.ilean +lib/lean/Lean/Meta/Tactic/Grind/EMatchTheorem.olean +lib/lean/Lean/Meta/Tactic/Grind/ENodeKey.ilean +lib/lean/Lean/Meta/Tactic/Grind/ENodeKey.olean +lib/lean/Lean/Meta/Tactic/Grind/EqResolution.ilean +lib/lean/Lean/Meta/Tactic/Grind/EqResolution.olean +lib/lean/Lean/Meta/Tactic/Grind/Ext.ilean +lib/lean/Lean/Meta/Tactic/Grind/Ext.olean +lib/lean/Lean/Meta/Tactic/Grind/ExtAttr.ilean +lib/lean/Lean/Meta/Tactic/Grind/ExtAttr.olean +lib/lean/Lean/Meta/Tactic/Grind/ForallProp.ilean +lib/lean/Lean/Meta/Tactic/Grind/ForallProp.olean lib/lean/Lean/Meta/Tactic/Grind/Injection.ilean lib/lean/Lean/Meta/Tactic/Grind/Injection.olean -lib/lean/Lean/Meta/Tactic/Grind/Preprocessor.ilean -lib/lean/Lean/Meta/Tactic/Grind/Preprocessor.olean +lib/lean/Lean/Meta/Tactic/Grind/Internalize.ilean +lib/lean/Lean/Meta/Tactic/Grind/Internalize.olean +lib/lean/Lean/Meta/Tactic/Grind/Intro.ilean +lib/lean/Lean/Meta/Tactic/Grind/Intro.olean +lib/lean/Lean/Meta/Tactic/Grind/Inv.ilean +lib/lean/Lean/Meta/Tactic/Grind/Inv.olean +lib/lean/Lean/Meta/Tactic/Grind/Lookahead.ilean +lib/lean/Lean/Meta/Tactic/Grind/Lookahead.olean +lib/lean/Lean/Meta/Tactic/Grind/MBTC.ilean +lib/lean/Lean/Meta/Tactic/Grind/MBTC.olean +lib/lean/Lean/Meta/Tactic/Grind/Main.ilean +lib/lean/Lean/Meta/Tactic/Grind/Main.olean +lib/lean/Lean/Meta/Tactic/Grind/MarkNestedProofs.ilean +lib/lean/Lean/Meta/Tactic/Grind/MarkNestedProofs.olean +lib/lean/Lean/Meta/Tactic/Grind/MatchCond.ilean +lib/lean/Lean/Meta/Tactic/Grind/MatchCond.olean +lib/lean/Lean/Meta/Tactic/Grind/MatchDiscrOnly.ilean +lib/lean/Lean/Meta/Tactic/Grind/MatchDiscrOnly.olean +lib/lean/Lean/Meta/Tactic/Grind/PP.ilean +lib/lean/Lean/Meta/Tactic/Grind/PP.olean +lib/lean/Lean/Meta/Tactic/Grind/Parser.ilean +lib/lean/Lean/Meta/Tactic/Grind/Parser.olean +lib/lean/Lean/Meta/Tactic/Grind/Proj.ilean +lib/lean/Lean/Meta/Tactic/Grind/Proj.olean +lib/lean/Lean/Meta/Tactic/Grind/Proof.ilean +lib/lean/Lean/Meta/Tactic/Grind/Proof.olean +lib/lean/Lean/Meta/Tactic/Grind/Propagate.ilean +lib/lean/Lean/Meta/Tactic/Grind/Propagate.olean +lib/lean/Lean/Meta/Tactic/Grind/PropagatorAttr.ilean +lib/lean/Lean/Meta/Tactic/Grind/PropagatorAttr.olean +lib/lean/Lean/Meta/Tactic/Grind/ProveEq.ilean +lib/lean/Lean/Meta/Tactic/Grind/ProveEq.olean lib/lean/Lean/Meta/Tactic/Grind/RevertAll.ilean lib/lean/Lean/Meta/Tactic/Grind/RevertAll.olean +lib/lean/Lean/Meta/Tactic/Grind/Simp.ilean +lib/lean/Lean/Meta/Tactic/Grind/Simp.olean +lib/lean/Lean/Meta/Tactic/Grind/SimpUtil.ilean +lib/lean/Lean/Meta/Tactic/Grind/SimpUtil.olean +lib/lean/Lean/Meta/Tactic/Grind/Solve.ilean +lib/lean/Lean/Meta/Tactic/Grind/Solve.olean +lib/lean/Lean/Meta/Tactic/Grind/Split.ilean +lib/lean/Lean/Meta/Tactic/Grind/Split.olean lib/lean/Lean/Meta/Tactic/Grind/Types.ilean lib/lean/Lean/Meta/Tactic/Grind/Types.olean lib/lean/Lean/Meta/Tactic/Grind/Util.ilean @@ -1625,26 +2723,10 @@ lib/lean/Lean/Meta/Tactic/Injection.ilean lib/lean/Lean/Meta/Tactic/Injection.olean lib/lean/Lean/Meta/Tactic/Intro.ilean lib/lean/Lean/Meta/Tactic/Intro.olean +lib/lean/Lean/Meta/Tactic/Lets.ilean +lib/lean/Lean/Meta/Tactic/Lets.olean lib/lean/Lean/Meta/Tactic/LibrarySearch.ilean lib/lean/Lean/Meta/Tactic/LibrarySearch.olean -lib/lean/Lean/Meta/Tactic/LinearArith.ilean -lib/lean/Lean/Meta/Tactic/LinearArith.olean -lib/lean/Lean/Meta/Tactic/LinearArith/Basic.ilean -lib/lean/Lean/Meta/Tactic/LinearArith/Basic.olean -lib/lean/Lean/Meta/Tactic/LinearArith/Main.ilean -lib/lean/Lean/Meta/Tactic/LinearArith/Main.olean -lib/lean/Lean/Meta/Tactic/LinearArith/Nat.ilean -lib/lean/Lean/Meta/Tactic/LinearArith/Nat.olean -lib/lean/Lean/Meta/Tactic/LinearArith/Nat/Basic.ilean -lib/lean/Lean/Meta/Tactic/LinearArith/Nat/Basic.olean -lib/lean/Lean/Meta/Tactic/LinearArith/Nat/Simp.ilean -lib/lean/Lean/Meta/Tactic/LinearArith/Nat/Simp.olean -lib/lean/Lean/Meta/Tactic/LinearArith/Nat/Solver.ilean -lib/lean/Lean/Meta/Tactic/LinearArith/Nat/Solver.olean -lib/lean/Lean/Meta/Tactic/LinearArith/Simp.ilean -lib/lean/Lean/Meta/Tactic/LinearArith/Simp.olean -lib/lean/Lean/Meta/Tactic/LinearArith/Solver.ilean -lib/lean/Lean/Meta/Tactic/LinearArith/Solver.olean lib/lean/Lean/Meta/Tactic/NormCast.ilean lib/lean/Lean/Meta/Tactic/NormCast.olean lib/lean/Lean/Meta/Tactic/Refl.ilean @@ -1665,6 +2747,22 @@ lib/lean/Lean/Meta/Tactic/Rfl.ilean lib/lean/Lean/Meta/Tactic/Rfl.olean lib/lean/Lean/Meta/Tactic/Simp.ilean lib/lean/Lean/Meta/Tactic/Simp.olean +lib/lean/Lean/Meta/Tactic/Simp/Arith.ilean +lib/lean/Lean/Meta/Tactic/Simp/Arith.olean +lib/lean/Lean/Meta/Tactic/Simp/Arith/Int.ilean +lib/lean/Lean/Meta/Tactic/Simp/Arith/Int.olean +lib/lean/Lean/Meta/Tactic/Simp/Arith/Int/Basic.ilean +lib/lean/Lean/Meta/Tactic/Simp/Arith/Int/Basic.olean +lib/lean/Lean/Meta/Tactic/Simp/Arith/Int/Simp.ilean +lib/lean/Lean/Meta/Tactic/Simp/Arith/Int/Simp.olean +lib/lean/Lean/Meta/Tactic/Simp/Arith/Nat.ilean +lib/lean/Lean/Meta/Tactic/Simp/Arith/Nat.olean +lib/lean/Lean/Meta/Tactic/Simp/Arith/Nat/Basic.ilean +lib/lean/Lean/Meta/Tactic/Simp/Arith/Nat/Basic.olean +lib/lean/Lean/Meta/Tactic/Simp/Arith/Nat/Simp.ilean +lib/lean/Lean/Meta/Tactic/Simp/Arith/Nat/Simp.olean +lib/lean/Lean/Meta/Tactic/Simp/Arith/Util.ilean +lib/lean/Lean/Meta/Tactic/Simp/Arith/Util.olean lib/lean/Lean/Meta/Tactic/Simp/Attr.ilean lib/lean/Lean/Meta/Tactic/Simp/Attr.olean lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs.ilean @@ -1685,6 +2783,8 @@ lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/List.ilean lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/List.olean lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.ilean lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.olean +lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/SInt.ilean +lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/SInt.olean lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/String.ilean lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/String.olean lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/UInt.ilean @@ -1719,6 +2819,10 @@ lib/lean/Lean/Meta/Tactic/Subst.ilean lib/lean/Lean/Meta/Tactic/Subst.olean lib/lean/Lean/Meta/Tactic/Symm.ilean lib/lean/Lean/Meta/Tactic/Symm.olean +lib/lean/Lean/Meta/Tactic/Try.ilean +lib/lean/Lean/Meta/Tactic/Try.olean +lib/lean/Lean/Meta/Tactic/Try/Collect.ilean +lib/lean/Lean/Meta/Tactic/Try/Collect.olean lib/lean/Lean/Meta/Tactic/TryThis.ilean lib/lean/Lean/Meta/Tactic/TryThis.olean lib/lean/Lean/Meta/Tactic/Unfold.ilean @@ -1741,6 +2845,8 @@ lib/lean/Lean/Modifiers.ilean lib/lean/Lean/Modifiers.olean lib/lean/Lean/MonadEnv.ilean lib/lean/Lean/MonadEnv.olean +lib/lean/Lean/Namespace.ilean +lib/lean/Lean/Namespace.olean lib/lean/Lean/Parser.ilean lib/lean/Lean/Parser.olean lib/lean/Lean/Parser/Attr.ilean @@ -1769,12 +2875,16 @@ lib/lean/Lean/Parser/Tactic/Doc.ilean lib/lean/Lean/Parser/Tactic/Doc.olean lib/lean/Lean/Parser/Term.ilean lib/lean/Lean/Parser/Term.olean +lib/lean/Lean/Parser/Term/Doc.ilean +lib/lean/Lean/Parser/Term/Doc.olean lib/lean/Lean/Parser/Types.ilean lib/lean/Lean/Parser/Types.olean lib/lean/Lean/ParserCompiler.ilean lib/lean/Lean/ParserCompiler.olean lib/lean/Lean/ParserCompiler/Attribute.ilean lib/lean/Lean/ParserCompiler/Attribute.olean +lib/lean/Lean/PremiseSelection.ilean +lib/lean/Lean/PremiseSelection.olean lib/lean/Lean/PrettyPrinter.ilean lib/lean/Lean/PrettyPrinter.olean lib/lean/Lean/PrettyPrinter/Basic.ilean @@ -1799,6 +2909,8 @@ lib/lean/Lean/PrettyPrinter/Formatter.ilean lib/lean/Lean/PrettyPrinter/Formatter.olean lib/lean/Lean/PrettyPrinter/Parenthesizer.ilean lib/lean/Lean/PrettyPrinter/Parenthesizer.olean +lib/lean/Lean/PrivateName.ilean +lib/lean/Lean/PrivateName.olean lib/lean/Lean/ProjFns.ilean lib/lean/Lean/ProjFns.olean lib/lean/Lean/ReducibilityAttrs.ilean @@ -1825,16 +2937,38 @@ lib/lean/Lean/Server/CodeActions/Basic.ilean lib/lean/Lean/Server/CodeActions/Basic.olean lib/lean/Lean/Server/CodeActions/Provider.ilean lib/lean/Lean/Server/CodeActions/Provider.olean +lib/lean/Lean/Server/CodeActions/UnknownIdentifier.ilean +lib/lean/Lean/Server/CodeActions/UnknownIdentifier.olean lib/lean/Lean/Server/Completion.ilean lib/lean/Lean/Server/Completion.olean -lib/lean/Lean/Server/CompletionItemData.ilean -lib/lean/Lean/Server/CompletionItemData.olean +lib/lean/Lean/Server/Completion/CompletionCollectors.ilean +lib/lean/Lean/Server/Completion/CompletionCollectors.olean +lib/lean/Lean/Server/Completion/CompletionInfoSelection.ilean +lib/lean/Lean/Server/Completion/CompletionInfoSelection.olean +lib/lean/Lean/Server/Completion/CompletionItemData.ilean +lib/lean/Lean/Server/Completion/CompletionItemData.olean +lib/lean/Lean/Server/Completion/CompletionResolution.ilean +lib/lean/Lean/Server/Completion/CompletionResolution.olean +lib/lean/Lean/Server/Completion/CompletionUtils.ilean +lib/lean/Lean/Server/Completion/CompletionUtils.olean +lib/lean/Lean/Server/Completion/EligibleHeaderDecls.ilean +lib/lean/Lean/Server/Completion/EligibleHeaderDecls.olean +lib/lean/Lean/Server/Completion/ImportCompletion.ilean +lib/lean/Lean/Server/Completion/ImportCompletion.olean +lib/lean/Lean/Server/Completion/SyntheticCompletion.ilean +lib/lean/Lean/Server/Completion/SyntheticCompletion.olean lib/lean/Lean/Server/FileSource.ilean lib/lean/Lean/Server/FileSource.olean lib/lean/Lean/Server/FileWorker.ilean lib/lean/Lean/Server/FileWorker.olean +lib/lean/Lean/Server/FileWorker/ExampleHover.ilean +lib/lean/Lean/Server/FileWorker/ExampleHover.olean +lib/lean/Lean/Server/FileWorker/InlayHints.ilean +lib/lean/Lean/Server/FileWorker/InlayHints.olean lib/lean/Lean/Server/FileWorker/RequestHandling.ilean lib/lean/Lean/Server/FileWorker/RequestHandling.olean +lib/lean/Lean/Server/FileWorker/SemanticHighlighting.ilean +lib/lean/Lean/Server/FileWorker/SemanticHighlighting.olean lib/lean/Lean/Server/FileWorker/SetupFile.ilean lib/lean/Lean/Server/FileWorker/SetupFile.olean lib/lean/Lean/Server/FileWorker/Utils.ilean @@ -1843,12 +2977,12 @@ lib/lean/Lean/Server/FileWorker/WidgetRequests.ilean lib/lean/Lean/Server/FileWorker/WidgetRequests.olean lib/lean/Lean/Server/GoTo.ilean lib/lean/Lean/Server/GoTo.olean -lib/lean/Lean/Server/ImportCompletion.ilean -lib/lean/Lean/Server/ImportCompletion.olean lib/lean/Lean/Server/InfoUtils.ilean lib/lean/Lean/Server/InfoUtils.olean lib/lean/Lean/Server/References.ilean lib/lean/Lean/Server/References.olean +lib/lean/Lean/Server/RequestCancellation.ilean +lib/lean/Lean/Server/RequestCancellation.olean lib/lean/Lean/Server/Requests.ilean lib/lean/Lean/Server/Requests.olean lib/lean/Lean/Server/Rpc.ilean @@ -1859,8 +2993,16 @@ lib/lean/Lean/Server/Rpc/Deriving.ilean lib/lean/Lean/Server/Rpc/Deriving.olean lib/lean/Lean/Server/Rpc/RequestHandling.ilean lib/lean/Lean/Server/Rpc/RequestHandling.olean +lib/lean/Lean/Server/ServerTask.ilean +lib/lean/Lean/Server/ServerTask.olean lib/lean/Lean/Server/Snapshots.ilean lib/lean/Lean/Server/Snapshots.olean +lib/lean/Lean/Server/Test.ilean +lib/lean/Lean/Server/Test.olean +lib/lean/Lean/Server/Test/Cancel.ilean +lib/lean/Lean/Server/Test/Cancel.olean +lib/lean/Lean/Server/Test/Runner.ilean +lib/lean/Lean/Server/Test/Runner.olean lib/lean/Lean/Server/Utils.ilean lib/lean/Lean/Server/Utils.olean lib/lean/Lean/Server/Watchdog.ilean @@ -1873,18 +3015,24 @@ lib/lean/Lean/Syntax.ilean lib/lean/Lean/Syntax.olean lib/lean/Lean/ToExpr.ilean lib/lean/Lean/ToExpr.olean +lib/lean/Lean/ToLevel.ilean +lib/lean/Lean/ToLevel.olean lib/lean/Lean/Util.ilean lib/lean/Lean/Util.olean lib/lean/Lean/Util/CollectAxioms.ilean lib/lean/Lean/Util/CollectAxioms.olean lib/lean/Lean/Util/CollectFVars.ilean lib/lean/Lean/Util/CollectFVars.olean +lib/lean/Lean/Util/CollectLevelMVars.ilean +lib/lean/Lean/Util/CollectLevelMVars.olean lib/lean/Lean/Util/CollectLevelParams.ilean lib/lean/Lean/Util/CollectLevelParams.olean lib/lean/Lean/Util/CollectMVars.ilean lib/lean/Lean/Util/CollectMVars.olean lib/lean/Lean/Util/Diff.ilean lib/lean/Lean/Util/Diff.olean +lib/lean/Lean/Util/FVarSubset.ilean +lib/lean/Lean/Util/FVarSubset.olean lib/lean/Lean/Util/FileSetupInfo.ilean lib/lean/Lean/Util/FileSetupInfo.olean lib/lean/Lean/Util/FindExpr.ilean @@ -1949,6 +3097,8 @@ lib/lean/Lean/Util/ShareCommon.ilean lib/lean/Lean/Util/ShareCommon.olean lib/lean/Lean/Util/Sorry.ilean lib/lean/Lean/Util/Sorry.olean +lib/lean/Lean/Util/SortExprs.ilean +lib/lean/Lean/Util/SortExprs.olean lib/lean/Lean/Util/TestExtern.ilean lib/lean/Lean/Util/TestExtern.olean lib/lean/Lean/Util/Trace.ilean @@ -1973,6 +3123,10 @@ lib/lean/Lean/Widget/UserWidget.ilean lib/lean/Lean/Widget/UserWidget.olean lib/lean/Std.ilean lib/lean/Std.olean +lib/lean/Std/Classes.ilean +lib/lean/Std/Classes.olean +lib/lean/Std/Classes/Ord.ilean +lib/lean/Std/Classes/Ord.olean lib/lean/Std/Data.ilean lib/lean/Std/Data.olean lib/lean/Std/Data/DHashMap.ilean @@ -1987,18 +3141,10 @@ lib/lean/Std/Data/DHashMap/Internal/AssocList/Lemmas.ilean lib/lean/Std/Data/DHashMap/Internal/AssocList/Lemmas.olean lib/lean/Std/Data/DHashMap/Internal/Defs.ilean lib/lean/Std/Data/DHashMap/Internal/Defs.olean +lib/lean/Std/Data/DHashMap/Internal/HashesTo.ilean +lib/lean/Std/Data/DHashMap/Internal/HashesTo.olean lib/lean/Std/Data/DHashMap/Internal/Index.ilean lib/lean/Std/Data/DHashMap/Internal/Index.olean -lib/lean/Std/Data/DHashMap/Internal/List/Associative.ilean -lib/lean/Std/Data/DHashMap/Internal/List/Associative.olean -lib/lean/Std/Data/DHashMap/Internal/List/Defs.ilean -lib/lean/Std/Data/DHashMap/Internal/List/Defs.olean -lib/lean/Std/Data/DHashMap/Internal/List/HashesTo.ilean -lib/lean/Std/Data/DHashMap/Internal/List/HashesTo.olean -lib/lean/Std/Data/DHashMap/Internal/List/Pairwise.ilean -lib/lean/Std/Data/DHashMap/Internal/List/Pairwise.olean -lib/lean/Std/Data/DHashMap/Internal/List/Sublist.ilean -lib/lean/Std/Data/DHashMap/Internal/List/Sublist.olean lib/lean/Std/Data/DHashMap/Internal/Model.ilean lib/lean/Std/Data/DHashMap/Internal/Model.olean lib/lean/Std/Data/DHashMap/Internal/Raw.ilean @@ -2015,6 +3161,64 @@ lib/lean/Std/Data/DHashMap/RawDef.ilean lib/lean/Std/Data/DHashMap/RawDef.olean lib/lean/Std/Data/DHashMap/RawLemmas.ilean lib/lean/Std/Data/DHashMap/RawLemmas.olean +lib/lean/Std/Data/DTreeMap.ilean +lib/lean/Std/Data/DTreeMap.olean +lib/lean/Std/Data/DTreeMap/AdditionalOperations.ilean +lib/lean/Std/Data/DTreeMap/AdditionalOperations.olean +lib/lean/Std/Data/DTreeMap/Basic.ilean +lib/lean/Std/Data/DTreeMap/Basic.olean +lib/lean/Std/Data/DTreeMap/Internal/Balanced.ilean +lib/lean/Std/Data/DTreeMap/Internal/Balanced.olean +lib/lean/Std/Data/DTreeMap/Internal/Balancing.ilean +lib/lean/Std/Data/DTreeMap/Internal/Balancing.olean +lib/lean/Std/Data/DTreeMap/Internal/Cell.ilean +lib/lean/Std/Data/DTreeMap/Internal/Cell.olean +lib/lean/Std/Data/DTreeMap/Internal/Def.ilean +lib/lean/Std/Data/DTreeMap/Internal/Def.olean +lib/lean/Std/Data/DTreeMap/Internal/Lemmas.ilean +lib/lean/Std/Data/DTreeMap/Internal/Lemmas.olean +lib/lean/Std/Data/DTreeMap/Internal/Model.ilean +lib/lean/Std/Data/DTreeMap/Internal/Model.olean +lib/lean/Std/Data/DTreeMap/Internal/Operations.ilean +lib/lean/Std/Data/DTreeMap/Internal/Operations.olean +lib/lean/Std/Data/DTreeMap/Internal/Ordered.ilean +lib/lean/Std/Data/DTreeMap/Internal/Ordered.olean +lib/lean/Std/Data/DTreeMap/Internal/Queries.ilean +lib/lean/Std/Data/DTreeMap/Internal/Queries.olean +lib/lean/Std/Data/DTreeMap/Internal/WF/Defs.ilean +lib/lean/Std/Data/DTreeMap/Internal/WF/Defs.olean +lib/lean/Std/Data/DTreeMap/Internal/WF/Lemmas.ilean +lib/lean/Std/Data/DTreeMap/Internal/WF/Lemmas.olean +lib/lean/Std/Data/DTreeMap/Lemmas.ilean +lib/lean/Std/Data/DTreeMap/Lemmas.olean +lib/lean/Std/Data/DTreeMap/Raw.ilean +lib/lean/Std/Data/DTreeMap/Raw.olean +lib/lean/Std/Data/DTreeMap/Raw/AdditionalOperations.ilean +lib/lean/Std/Data/DTreeMap/Raw/AdditionalOperations.olean +lib/lean/Std/Data/DTreeMap/Raw/Basic.ilean +lib/lean/Std/Data/DTreeMap/Raw/Basic.olean +lib/lean/Std/Data/DTreeMap/Raw/Lemmas.ilean +lib/lean/Std/Data/DTreeMap/Raw/Lemmas.olean +lib/lean/Std/Data/DTreeMap/Raw/WF.ilean +lib/lean/Std/Data/DTreeMap/Raw/WF.olean +lib/lean/Std/Data/ExtDHashMap.ilean +lib/lean/Std/Data/ExtDHashMap.olean +lib/lean/Std/Data/ExtDHashMap/Basic.ilean +lib/lean/Std/Data/ExtDHashMap/Basic.olean +lib/lean/Std/Data/ExtDHashMap/Lemmas.ilean +lib/lean/Std/Data/ExtDHashMap/Lemmas.olean +lib/lean/Std/Data/ExtHashMap.ilean +lib/lean/Std/Data/ExtHashMap.olean +lib/lean/Std/Data/ExtHashMap/Basic.ilean +lib/lean/Std/Data/ExtHashMap/Basic.olean +lib/lean/Std/Data/ExtHashMap/Lemmas.ilean +lib/lean/Std/Data/ExtHashMap/Lemmas.olean +lib/lean/Std/Data/ExtHashSet.ilean +lib/lean/Std/Data/ExtHashSet.olean +lib/lean/Std/Data/ExtHashSet/Basic.ilean +lib/lean/Std/Data/ExtHashSet/Basic.olean +lib/lean/Std/Data/ExtHashSet/Lemmas.ilean +lib/lean/Std/Data/ExtHashSet/Lemmas.olean lib/lean/Std/Data/HashMap.ilean lib/lean/Std/Data/HashMap.olean lib/lean/Std/Data/HashMap/AdditionalOperations.ilean @@ -2037,8 +3241,60 @@ lib/lean/Std/Data/HashSet/Raw.ilean lib/lean/Std/Data/HashSet/Raw.olean lib/lean/Std/Data/HashSet/RawLemmas.ilean lib/lean/Std/Data/HashSet/RawLemmas.olean +lib/lean/Std/Data/Internal/Cut.ilean +lib/lean/Std/Data/Internal/Cut.olean +lib/lean/Std/Data/Internal/List/Associative.ilean +lib/lean/Std/Data/Internal/List/Associative.olean +lib/lean/Std/Data/Internal/List/Defs.ilean +lib/lean/Std/Data/Internal/List/Defs.olean +lib/lean/Std/Data/TreeMap.ilean +lib/lean/Std/Data/TreeMap.olean +lib/lean/Std/Data/TreeMap/AdditionalOperations.ilean +lib/lean/Std/Data/TreeMap/AdditionalOperations.olean +lib/lean/Std/Data/TreeMap/Basic.ilean +lib/lean/Std/Data/TreeMap/Basic.olean +lib/lean/Std/Data/TreeMap/Lemmas.ilean +lib/lean/Std/Data/TreeMap/Lemmas.olean +lib/lean/Std/Data/TreeMap/Raw.ilean +lib/lean/Std/Data/TreeMap/Raw.olean +lib/lean/Std/Data/TreeMap/Raw/AdditionalOperations.ilean +lib/lean/Std/Data/TreeMap/Raw/AdditionalOperations.olean +lib/lean/Std/Data/TreeMap/Raw/Basic.ilean +lib/lean/Std/Data/TreeMap/Raw/Basic.olean +lib/lean/Std/Data/TreeMap/Raw/Lemmas.ilean +lib/lean/Std/Data/TreeMap/Raw/Lemmas.olean +lib/lean/Std/Data/TreeMap/Raw/WF.ilean +lib/lean/Std/Data/TreeMap/Raw/WF.olean +lib/lean/Std/Data/TreeSet.ilean +lib/lean/Std/Data/TreeSet.olean +lib/lean/Std/Data/TreeSet/AdditionalOperations.ilean +lib/lean/Std/Data/TreeSet/AdditionalOperations.olean +lib/lean/Std/Data/TreeSet/Basic.ilean +lib/lean/Std/Data/TreeSet/Basic.olean +lib/lean/Std/Data/TreeSet/Lemmas.ilean +lib/lean/Std/Data/TreeSet/Lemmas.olean +lib/lean/Std/Data/TreeSet/Raw.ilean +lib/lean/Std/Data/TreeSet/Raw.olean +lib/lean/Std/Data/TreeSet/Raw/Basic.ilean +lib/lean/Std/Data/TreeSet/Raw/Basic.olean +lib/lean/Std/Data/TreeSet/Raw/Lemmas.ilean +lib/lean/Std/Data/TreeSet/Raw/Lemmas.olean +lib/lean/Std/Data/TreeSet/Raw/WF.ilean +lib/lean/Std/Data/TreeSet/Raw/WF.olean lib/lean/Std/Internal.ilean lib/lean/Std/Internal.olean +lib/lean/Std/Internal/Async.ilean +lib/lean/Std/Internal/Async.olean +lib/lean/Std/Internal/Async/Basic.ilean +lib/lean/Std/Internal/Async/Basic.olean +lib/lean/Std/Internal/Async/Select.ilean +lib/lean/Std/Internal/Async/Select.olean +lib/lean/Std/Internal/Async/TCP.ilean +lib/lean/Std/Internal/Async/TCP.olean +lib/lean/Std/Internal/Async/Timer.ilean +lib/lean/Std/Internal/Async/Timer.olean +lib/lean/Std/Internal/Async/UDP.ilean +lib/lean/Std/Internal/Async/UDP.olean lib/lean/Std/Internal/Parsec.ilean lib/lean/Std/Internal/Parsec.olean lib/lean/Std/Internal/Parsec/Basic.ilean @@ -2047,6 +3303,22 @@ lib/lean/Std/Internal/Parsec/ByteArray.ilean lib/lean/Std/Internal/Parsec/ByteArray.olean lib/lean/Std/Internal/Parsec/String.ilean lib/lean/Std/Internal/Parsec/String.olean +lib/lean/Std/Internal/Rat.ilean +lib/lean/Std/Internal/Rat.olean +lib/lean/Std/Internal/UV.ilean +lib/lean/Std/Internal/UV.olean +lib/lean/Std/Internal/UV/Loop.ilean +lib/lean/Std/Internal/UV/Loop.olean +lib/lean/Std/Internal/UV/TCP.ilean +lib/lean/Std/Internal/UV/TCP.olean +lib/lean/Std/Internal/UV/Timer.ilean +lib/lean/Std/Internal/UV/Timer.olean +lib/lean/Std/Internal/UV/UDP.ilean +lib/lean/Std/Internal/UV/UDP.olean +lib/lean/Std/Net.ilean +lib/lean/Std/Net.olean +lib/lean/Std/Net/Addr.ilean +lib/lean/Std/Net/Addr.olean lib/lean/Std/Sat.ilean lib/lean/Std/Sat.olean lib/lean/Std/Sat/AIG.ilean @@ -2097,6 +3369,20 @@ lib/lean/Std/Sat/CNF/Relabel.ilean lib/lean/Std/Sat/CNF/Relabel.olean lib/lean/Std/Sat/CNF/RelabelFin.ilean lib/lean/Std/Sat/CNF/RelabelFin.olean +lib/lean/Std/Sync.ilean +lib/lean/Std/Sync.olean +lib/lean/Std/Sync/Barrier.ilean +lib/lean/Std/Sync/Barrier.olean +lib/lean/Std/Sync/Basic.ilean +lib/lean/Std/Sync/Basic.olean +lib/lean/Std/Sync/Channel.ilean +lib/lean/Std/Sync/Channel.olean +lib/lean/Std/Sync/Mutex.ilean +lib/lean/Std/Sync/Mutex.olean +lib/lean/Std/Sync/RecursiveMutex.ilean +lib/lean/Std/Sync/RecursiveMutex.olean +lib/lean/Std/Sync/SharedMutex.ilean +lib/lean/Std/Sync/SharedMutex.olean lib/lean/Std/Tactic.ilean lib/lean/Std/Tactic.olean lib/lean/Std/Tactic/BVDecide.ilean @@ -2117,8 +3403,6 @@ lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Const.ilean lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Const.olean lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Expr.ilean lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Expr.olean -lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations.ilean -lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations.olean lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Add.ilean lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Add.olean lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Append.ilean @@ -2131,6 +3415,8 @@ lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/GetLsbD.ile lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/GetLsbD.olean lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Mul.ilean lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Mul.olean +lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Neg.ilean +lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Neg.olean lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Not.ilean lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Not.olean lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Replicate.ilean @@ -2143,14 +3429,20 @@ lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/ShiftLeft.i lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/ShiftLeft.olean lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/ShiftRight.ilean lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/ShiftRight.olean -lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/SignExtend.ilean -lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/SignExtend.olean +lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Sub.ilean +lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Sub.olean +lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Udiv.ilean +lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Udiv.olean lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Ult.ilean lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Ult.olean +lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Umod.ilean +lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Umod.olean lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/ZeroExtend.ilean lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/ZeroExtend.olean lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Pred.ilean lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Pred.olean +lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Substructure.ilean +lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Substructure.olean lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Var.ilean lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Var.olean lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas.ilean @@ -2163,8 +3455,6 @@ lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Const.ilean lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Const.olean lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.ilean lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.olean -lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations.ilean -lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations.olean lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Add.ilean lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Add.olean lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Append.ilean @@ -2177,6 +3467,8 @@ lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/GetLsbD.i lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/GetLsbD.olean lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Mul.ilean lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Mul.olean +lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Neg.ilean +lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Neg.olean lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Not.ilean lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Not.olean lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Replicate.ilean @@ -2189,10 +3481,14 @@ lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftLeft lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftLeft.olean lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftRight.ilean lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftRight.olean -lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/SignExtend.ilean -lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/SignExtend.olean +lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Sub.ilean +lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Sub.olean +lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Udiv.ilean +lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Udiv.olean lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Ult.ilean lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Ult.olean +lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Umod.ilean +lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Umod.olean lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ZeroExtend.ilean lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ZeroExtend.olean lib/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Pred.ilean @@ -2203,16 +3499,12 @@ lib/lean/Std/Tactic/BVDecide/Bitblast/BoolExpr.ilean lib/lean/Std/Tactic/BVDecide/Bitblast/BoolExpr.olean lib/lean/Std/Tactic/BVDecide/Bitblast/BoolExpr/Basic.ilean lib/lean/Std/Tactic/BVDecide/Bitblast/BoolExpr/Basic.olean -lib/lean/Std/Tactic/BVDecide/Bitblast/BoolExpr/Circuit.ilean -lib/lean/Std/Tactic/BVDecide/Bitblast/BoolExpr/Circuit.olean lib/lean/Std/Tactic/BVDecide/LRAT.ilean lib/lean/Std/Tactic/BVDecide/LRAT.olean lib/lean/Std/Tactic/BVDecide/LRAT/Actions.ilean lib/lean/Std/Tactic/BVDecide/LRAT/Actions.olean lib/lean/Std/Tactic/BVDecide/LRAT/Checker.ilean lib/lean/Std/Tactic/BVDecide/LRAT/Checker.olean -lib/lean/Std/Tactic/BVDecide/LRAT/Internal.ilean -lib/lean/Std/Tactic/BVDecide/LRAT/Internal.olean lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Actions.ilean lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Actions.olean lib/lean/Std/Tactic/BVDecide/LRAT/Internal/Assignment.ilean @@ -2267,9 +3559,96 @@ lib/lean/Std/Tactic/BVDecide/Reflect.ilean lib/lean/Std/Tactic/BVDecide/Reflect.olean lib/lean/Std/Tactic/BVDecide/Syntax.ilean lib/lean/Std/Tactic/BVDecide/Syntax.olean +lib/lean/Std/Time.ilean +lib/lean/Std/Time.olean +lib/lean/Std/Time/Date.ilean +lib/lean/Std/Time/Date.olean +lib/lean/Std/Time/Date/Basic.ilean +lib/lean/Std/Time/Date/Basic.olean +lib/lean/Std/Time/Date/PlainDate.ilean +lib/lean/Std/Time/Date/PlainDate.olean +lib/lean/Std/Time/Date/Unit/Basic.ilean +lib/lean/Std/Time/Date/Unit/Basic.olean +lib/lean/Std/Time/Date/Unit/Day.ilean +lib/lean/Std/Time/Date/Unit/Day.olean +lib/lean/Std/Time/Date/Unit/Month.ilean +lib/lean/Std/Time/Date/Unit/Month.olean +lib/lean/Std/Time/Date/Unit/Week.ilean +lib/lean/Std/Time/Date/Unit/Week.olean +lib/lean/Std/Time/Date/Unit/Weekday.ilean +lib/lean/Std/Time/Date/Unit/Weekday.olean +lib/lean/Std/Time/Date/Unit/Year.ilean +lib/lean/Std/Time/Date/Unit/Year.olean +lib/lean/Std/Time/Date/ValidDate.ilean +lib/lean/Std/Time/Date/ValidDate.olean +lib/lean/Std/Time/DateTime.ilean +lib/lean/Std/Time/DateTime.olean +lib/lean/Std/Time/DateTime/PlainDateTime.ilean +lib/lean/Std/Time/DateTime/PlainDateTime.olean +lib/lean/Std/Time/DateTime/Timestamp.ilean +lib/lean/Std/Time/DateTime/Timestamp.olean +lib/lean/Std/Time/Duration.ilean +lib/lean/Std/Time/Duration.olean +lib/lean/Std/Time/Format.ilean +lib/lean/Std/Time/Format.olean +lib/lean/Std/Time/Format/Basic.ilean +lib/lean/Std/Time/Format/Basic.olean +lib/lean/Std/Time/Internal.ilean +lib/lean/Std/Time/Internal.olean +lib/lean/Std/Time/Internal/Bounded.ilean +lib/lean/Std/Time/Internal/Bounded.olean +lib/lean/Std/Time/Internal/UnitVal.ilean +lib/lean/Std/Time/Internal/UnitVal.olean +lib/lean/Std/Time/Notation.ilean +lib/lean/Std/Time/Notation.olean +lib/lean/Std/Time/Notation/Spec.ilean +lib/lean/Std/Time/Notation/Spec.olean +lib/lean/Std/Time/Time.ilean +lib/lean/Std/Time/Time.olean +lib/lean/Std/Time/Time/Basic.ilean +lib/lean/Std/Time/Time/Basic.olean +lib/lean/Std/Time/Time/HourMarker.ilean +lib/lean/Std/Time/Time/HourMarker.olean +lib/lean/Std/Time/Time/PlainTime.ilean +lib/lean/Std/Time/Time/PlainTime.olean +lib/lean/Std/Time/Time/Unit/Basic.ilean +lib/lean/Std/Time/Time/Unit/Basic.olean +lib/lean/Std/Time/Time/Unit/Hour.ilean +lib/lean/Std/Time/Time/Unit/Hour.olean +lib/lean/Std/Time/Time/Unit/Millisecond.ilean +lib/lean/Std/Time/Time/Unit/Millisecond.olean +lib/lean/Std/Time/Time/Unit/Minute.ilean +lib/lean/Std/Time/Time/Unit/Minute.olean +lib/lean/Std/Time/Time/Unit/Nanosecond.ilean +lib/lean/Std/Time/Time/Unit/Nanosecond.olean +lib/lean/Std/Time/Time/Unit/Second.ilean +lib/lean/Std/Time/Time/Unit/Second.olean +lib/lean/Std/Time/Zoned.ilean +lib/lean/Std/Time/Zoned.olean +lib/lean/Std/Time/Zoned/Database.ilean +lib/lean/Std/Time/Zoned/Database.olean +lib/lean/Std/Time/Zoned/Database/Basic.ilean +lib/lean/Std/Time/Zoned/Database/Basic.olean +lib/lean/Std/Time/Zoned/Database/TZdb.ilean +lib/lean/Std/Time/Zoned/Database/TZdb.olean +lib/lean/Std/Time/Zoned/Database/TzIf.ilean +lib/lean/Std/Time/Zoned/Database/TzIf.olean +lib/lean/Std/Time/Zoned/Database/Windows.ilean +lib/lean/Std/Time/Zoned/Database/Windows.olean +lib/lean/Std/Time/Zoned/DateTime.ilean +lib/lean/Std/Time/Zoned/DateTime.olean +lib/lean/Std/Time/Zoned/Offset.ilean +lib/lean/Std/Time/Zoned/Offset.olean +lib/lean/Std/Time/Zoned/TimeZone.ilean +lib/lean/Std/Time/Zoned/TimeZone.olean +lib/lean/Std/Time/Zoned/ZoneRules.ilean +lib/lean/Std/Time/Zoned/ZoneRules.olean +lib/lean/Std/Time/Zoned/ZonedDateTime.ilean +lib/lean/Std/Time/Zoned/ZonedDateTime.olean lib/lean/libInit.a lib/lean/libInit_shared.so lib/lean/libLake.a +lib/lean/libLake_shared.so lib/lean/libLean.a lib/lean/libStd.a lib/lean/libleancpp.a @@ -2279,6 +3658,7 @@ lib/lean/libleanshared.so lib/lean/libleanshared_1.so share/lean/lean.mk %%DATADIR%%/src/lean/Init.lean +%%DATADIR%%/src/lean/Init/BinderNameHint.lean %%DATADIR%%/src/lean/Init/BinderPredicates.lean %%DATADIR%%/src/lean/Init/ByCases.lean %%DATADIR%%/src/lean/Init/Classical.lean @@ -2292,6 +3672,7 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Init/Control/Lawful.lean %%DATADIR%%/src/lean/Init/Control/Lawful/Basic.lean %%DATADIR%%/src/lean/Init/Control/Lawful/Instances.lean +%%DATADIR%%/src/lean/Init/Control/Lawful/Lemmas.lean %%DATADIR%%/src/lean/Init/Control/Option.lean %%DATADIR%%/src/lean/Init/Control/Reader.lean %%DATADIR%%/src/lean/Init/Control/State.lean @@ -2306,18 +3687,38 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Init/Data/Array/Basic.lean %%DATADIR%%/src/lean/Init/Data/Array/BasicAux.lean %%DATADIR%%/src/lean/Init/Data/Array/BinSearch.lean +%%DATADIR%%/src/lean/Init/Data/Array/Bootstrap.lean +%%DATADIR%%/src/lean/Init/Data/Array/Count.lean %%DATADIR%%/src/lean/Init/Data/Array/DecidableEq.lean +%%DATADIR%%/src/lean/Init/Data/Array/Erase.lean +%%DATADIR%%/src/lean/Init/Data/Array/Extract.lean +%%DATADIR%%/src/lean/Init/Data/Array/FinRange.lean +%%DATADIR%%/src/lean/Init/Data/Array/Find.lean +%%DATADIR%%/src/lean/Init/Data/Array/GetLit.lean +%%DATADIR%%/src/lean/Init/Data/Array/InsertIdx.lean %%DATADIR%%/src/lean/Init/Data/Array/InsertionSort.lean %%DATADIR%%/src/lean/Init/Data/Array/Lemmas.lean +%%DATADIR%%/src/lean/Init/Data/Array/Lex.lean +%%DATADIR%%/src/lean/Init/Data/Array/Lex/Basic.lean +%%DATADIR%%/src/lean/Init/Data/Array/Lex/Lemmas.lean +%%DATADIR%%/src/lean/Init/Data/Array/MapIdx.lean %%DATADIR%%/src/lean/Init/Data/Array/Mem.lean +%%DATADIR%%/src/lean/Init/Data/Array/Monadic.lean +%%DATADIR%%/src/lean/Init/Data/Array/OfFn.lean +%%DATADIR%%/src/lean/Init/Data/Array/Perm.lean %%DATADIR%%/src/lean/Init/Data/Array/QSort.lean +%%DATADIR%%/src/lean/Init/Data/Array/QSort/Basic.lean +%%DATADIR%%/src/lean/Init/Data/Array/Range.lean +%%DATADIR%%/src/lean/Init/Data/Array/Set.lean %%DATADIR%%/src/lean/Init/Data/Array/Subarray.lean %%DATADIR%%/src/lean/Init/Data/Array/Subarray/Split.lean %%DATADIR%%/src/lean/Init/Data/Array/TakeDrop.lean +%%DATADIR%%/src/lean/Init/Data/Array/Zip.lean %%DATADIR%%/src/lean/Init/Data/BEq.lean %%DATADIR%%/src/lean/Init/Data/Basic.lean %%DATADIR%%/src/lean/Init/Data/BitVec.lean %%DATADIR%%/src/lean/Init/Data/BitVec/Basic.lean +%%DATADIR%%/src/lean/Init/Data/BitVec/BasicAux.lean %%DATADIR%%/src/lean/Init/Data/BitVec/Bitblast.lean %%DATADIR%%/src/lean/Init/Data/BitVec/Folds.lean %%DATADIR%%/src/lean/Init/Data/BitVec/Lemmas.lean @@ -2325,7 +3726,6 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Init/Data/ByteArray.lean %%DATADIR%%/src/lean/Init/Data/ByteArray/Basic.lean %%DATADIR%%/src/lean/Init/Data/Cast.lean -%%DATADIR%%/src/lean/Init/Data/Channel.lean %%DATADIR%%/src/lean/Init/Data/Char.lean %%DATADIR%%/src/lean/Init/Data/Char/Basic.lean %%DATADIR%%/src/lean/Init/Data/Char/Lemmas.lean @@ -2337,6 +3737,7 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Init/Data/Fin/Lemmas.lean %%DATADIR%%/src/lean/Init/Data/Fin/Log2.lean %%DATADIR%%/src/lean/Init/Data/Float.lean +%%DATADIR%%/src/lean/Init/Data/Float32.lean %%DATADIR%%/src/lean/Init/Data/FloatArray.lean %%DATADIR%%/src/lean/Init/Data/FloatArray/Basic.lean %%DATADIR%%/src/lean/Init/Data/Format.lean @@ -2344,16 +3745,24 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Init/Data/Format/Instances.lean %%DATADIR%%/src/lean/Init/Data/Format/Macro.lean %%DATADIR%%/src/lean/Init/Data/Format/Syntax.lean +%%DATADIR%%/src/lean/Init/Data/Function.lean %%DATADIR%%/src/lean/Init/Data/Hashable.lean %%DATADIR%%/src/lean/Init/Data/Int.lean %%DATADIR%%/src/lean/Init/Data/Int/Basic.lean %%DATADIR%%/src/lean/Init/Data/Int/Bitwise.lean +%%DATADIR%%/src/lean/Init/Data/Int/Bitwise/Basic.lean %%DATADIR%%/src/lean/Init/Data/Int/Bitwise/Lemmas.lean +%%DATADIR%%/src/lean/Init/Data/Int/Compare.lean +%%DATADIR%%/src/lean/Init/Data/Int/Cooper.lean %%DATADIR%%/src/lean/Init/Data/Int/DivMod.lean -%%DATADIR%%/src/lean/Init/Data/Int/DivModLemmas.lean +%%DATADIR%%/src/lean/Init/Data/Int/DivMod/Basic.lean +%%DATADIR%%/src/lean/Init/Data/Int/DivMod/Bootstrap.lean +%%DATADIR%%/src/lean/Init/Data/Int/DivMod/Lemmas.lean %%DATADIR%%/src/lean/Init/Data/Int/Gcd.lean %%DATADIR%%/src/lean/Init/Data/Int/Lemmas.lean %%DATADIR%%/src/lean/Init/Data/Int/LemmasAux.lean +%%DATADIR%%/src/lean/Init/Data/Int/Linear.lean +%%DATADIR%%/src/lean/Init/Data/Int/OfNat.lean %%DATADIR%%/src/lean/Init/Data/Int/Order.lean %%DATADIR%%/src/lean/Init/Data/Int/Pow.lean %%DATADIR%%/src/lean/Init/Data/List.lean @@ -2363,18 +3772,29 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Init/Data/List/Control.lean %%DATADIR%%/src/lean/Init/Data/List/Count.lean %%DATADIR%%/src/lean/Init/Data/List/Erase.lean +%%DATADIR%%/src/lean/Init/Data/List/FinRange.lean %%DATADIR%%/src/lean/Init/Data/List/Find.lean %%DATADIR%%/src/lean/Init/Data/List/Impl.lean %%DATADIR%%/src/lean/Init/Data/List/Lemmas.lean +%%DATADIR%%/src/lean/Init/Data/List/Lex.lean +%%DATADIR%%/src/lean/Init/Data/List/MapIdx.lean %%DATADIR%%/src/lean/Init/Data/List/MinMax.lean %%DATADIR%%/src/lean/Init/Data/List/Monadic.lean %%DATADIR%%/src/lean/Init/Data/List/Nat.lean +%%DATADIR%%/src/lean/Init/Data/List/Nat/BEq.lean %%DATADIR%%/src/lean/Init/Data/List/Nat/Basic.lean +%%DATADIR%%/src/lean/Init/Data/List/Nat/Count.lean +%%DATADIR%%/src/lean/Init/Data/List/Nat/Erase.lean +%%DATADIR%%/src/lean/Init/Data/List/Nat/Find.lean +%%DATADIR%%/src/lean/Init/Data/List/Nat/InsertIdx.lean +%%DATADIR%%/src/lean/Init/Data/List/Nat/Modify.lean %%DATADIR%%/src/lean/Init/Data/List/Nat/Pairwise.lean +%%DATADIR%%/src/lean/Init/Data/List/Nat/Perm.lean %%DATADIR%%/src/lean/Init/Data/List/Nat/Range.lean %%DATADIR%%/src/lean/Init/Data/List/Nat/Sublist.lean %%DATADIR%%/src/lean/Init/Data/List/Nat/TakeDrop.lean %%DATADIR%%/src/lean/Init/Data/List/Notation.lean +%%DATADIR%%/src/lean/Init/Data/List/OfFn.lean %%DATADIR%%/src/lean/Init/Data/List/Pairwise.lean %%DATADIR%%/src/lean/Init/Data/List/Perm.lean %%DATADIR%%/src/lean/Init/Data/List/Range.lean @@ -2384,6 +3804,8 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Init/Data/List/Sort/Lemmas.lean %%DATADIR%%/src/lean/Init/Data/List/Sublist.lean %%DATADIR%%/src/lean/Init/Data/List/TakeDrop.lean +%%DATADIR%%/src/lean/Init/Data/List/ToArray.lean +%%DATADIR%%/src/lean/Init/Data/List/ToArrayImpl.lean %%DATADIR%%/src/lean/Init/Data/List/Zip.lean %%DATADIR%%/src/lean/Init/Data/Nat.lean %%DATADIR%%/src/lean/Init/Data/Nat/Basic.lean @@ -2393,7 +3815,10 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Init/Data/Nat/Compare.lean %%DATADIR%%/src/lean/Init/Data/Nat/Control.lean %%DATADIR%%/src/lean/Init/Data/Nat/Div.lean +%%DATADIR%%/src/lean/Init/Data/Nat/Div/Basic.lean +%%DATADIR%%/src/lean/Init/Data/Nat/Div/Lemmas.lean %%DATADIR%%/src/lean/Init/Data/Nat/Dvd.lean +%%DATADIR%%/src/lean/Init/Data/Nat/Fold.lean %%DATADIR%%/src/lean/Init/Data/Nat/Gcd.lean %%DATADIR%%/src/lean/Init/Data/Nat/Lcm.lean %%DATADIR%%/src/lean/Init/Data/Nat/Lemmas.lean @@ -2404,19 +3829,33 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Init/Data/Nat/Power2.lean %%DATADIR%%/src/lean/Init/Data/Nat/SOM.lean %%DATADIR%%/src/lean/Init/Data/Nat/Simproc.lean +%%DATADIR%%/src/lean/Init/Data/NeZero.lean %%DATADIR%%/src/lean/Init/Data/OfScientific.lean %%DATADIR%%/src/lean/Init/Data/Option.lean +%%DATADIR%%/src/lean/Init/Data/Option/Attach.lean %%DATADIR%%/src/lean/Init/Data/Option/Basic.lean %%DATADIR%%/src/lean/Init/Data/Option/BasicAux.lean +%%DATADIR%%/src/lean/Init/Data/Option/Coe.lean %%DATADIR%%/src/lean/Init/Data/Option/Instances.lean %%DATADIR%%/src/lean/Init/Data/Option/Lemmas.lean +%%DATADIR%%/src/lean/Init/Data/Option/List.lean +%%DATADIR%%/src/lean/Init/Data/Option/Monadic.lean %%DATADIR%%/src/lean/Init/Data/Ord.lean %%DATADIR%%/src/lean/Init/Data/PLift.lean %%DATADIR%%/src/lean/Init/Data/Prod.lean %%DATADIR%%/src/lean/Init/Data/Queue.lean +%%DATADIR%%/src/lean/Init/Data/RArray.lean %%DATADIR%%/src/lean/Init/Data/Random.lean %%DATADIR%%/src/lean/Init/Data/Range.lean +%%DATADIR%%/src/lean/Init/Data/Range/Basic.lean +%%DATADIR%%/src/lean/Init/Data/Range/Lemmas.lean %%DATADIR%%/src/lean/Init/Data/Repr.lean +%%DATADIR%%/src/lean/Init/Data/SInt.lean +%%DATADIR%%/src/lean/Init/Data/SInt/Basic.lean +%%DATADIR%%/src/lean/Init/Data/SInt/Bitwise.lean +%%DATADIR%%/src/lean/Init/Data/SInt/Float.lean +%%DATADIR%%/src/lean/Init/Data/SInt/Float32.lean +%%DATADIR%%/src/lean/Init/Data/SInt/Lemmas.lean %%DATADIR%%/src/lean/Init/Data/Stream.lean %%DATADIR%%/src/lean/Init/Data/String.lean %%DATADIR%%/src/lean/Init/Data/String/Basic.lean @@ -2424,25 +3863,64 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Init/Data/String/Lemmas.lean %%DATADIR%%/src/lean/Init/Data/Subtype.lean %%DATADIR%%/src/lean/Init/Data/Sum.lean +%%DATADIR%%/src/lean/Init/Data/Sum/Basic.lean +%%DATADIR%%/src/lean/Init/Data/Sum/Lemmas.lean %%DATADIR%%/src/lean/Init/Data/ToString.lean %%DATADIR%%/src/lean/Init/Data/ToString/Basic.lean %%DATADIR%%/src/lean/Init/Data/ToString/Macro.lean %%DATADIR%%/src/lean/Init/Data/UInt.lean %%DATADIR%%/src/lean/Init/Data/UInt/Basic.lean +%%DATADIR%%/src/lean/Init/Data/UInt/BasicAux.lean %%DATADIR%%/src/lean/Init/Data/UInt/Bitwise.lean %%DATADIR%%/src/lean/Init/Data/UInt/Lemmas.lean %%DATADIR%%/src/lean/Init/Data/UInt/Log2.lean %%DATADIR%%/src/lean/Init/Data/ULift.lean +%%DATADIR%%/src/lean/Init/Data/Vector.lean +%%DATADIR%%/src/lean/Init/Data/Vector/Attach.lean +%%DATADIR%%/src/lean/Init/Data/Vector/Basic.lean +%%DATADIR%%/src/lean/Init/Data/Vector/Count.lean +%%DATADIR%%/src/lean/Init/Data/Vector/DecidableEq.lean +%%DATADIR%%/src/lean/Init/Data/Vector/Erase.lean +%%DATADIR%%/src/lean/Init/Data/Vector/Extract.lean +%%DATADIR%%/src/lean/Init/Data/Vector/FinRange.lean +%%DATADIR%%/src/lean/Init/Data/Vector/Find.lean +%%DATADIR%%/src/lean/Init/Data/Vector/InsertIdx.lean +%%DATADIR%%/src/lean/Init/Data/Vector/Lemmas.lean +%%DATADIR%%/src/lean/Init/Data/Vector/Lex.lean +%%DATADIR%%/src/lean/Init/Data/Vector/MapIdx.lean +%%DATADIR%%/src/lean/Init/Data/Vector/Monadic.lean +%%DATADIR%%/src/lean/Init/Data/Vector/OfFn.lean +%%DATADIR%%/src/lean/Init/Data/Vector/Perm.lean +%%DATADIR%%/src/lean/Init/Data/Vector/Range.lean +%%DATADIR%%/src/lean/Init/Data/Vector/Zip.lean +%%DATADIR%%/src/lean/Init/Data/Zero.lean %%DATADIR%%/src/lean/Init/Dynamic.lean %%DATADIR%%/src/lean/Init/Ext.lean %%DATADIR%%/src/lean/Init/GetElem.lean %%DATADIR%%/src/lean/Init/Grind.lean %%DATADIR%%/src/lean/Init/Grind/Cases.lean +%%DATADIR%%/src/lean/Init/Grind/CommRing.lean +%%DATADIR%%/src/lean/Init/Grind/CommRing/Basic.lean +%%DATADIR%%/src/lean/Init/Grind/CommRing/BitVec.lean +%%DATADIR%%/src/lean/Init/Grind/CommRing/Int.lean +%%DATADIR%%/src/lean/Init/Grind/CommRing/Poly.lean +%%DATADIR%%/src/lean/Init/Grind/CommRing/SInt.lean +%%DATADIR%%/src/lean/Init/Grind/CommRing/UInt.lean +%%DATADIR%%/src/lean/Init/Grind/Ext.lean %%DATADIR%%/src/lean/Init/Grind/Lemmas.lean %%DATADIR%%/src/lean/Init/Grind/Norm.lean +%%DATADIR%%/src/lean/Init/Grind/Offset.lean +%%DATADIR%%/src/lean/Init/Grind/PP.lean +%%DATADIR%%/src/lean/Init/Grind/Propagator.lean %%DATADIR%%/src/lean/Init/Grind/Tactics.lean +%%DATADIR%%/src/lean/Init/Grind/Util.lean %%DATADIR%%/src/lean/Init/Guard.lean %%DATADIR%%/src/lean/Init/Hints.lean +%%DATADIR%%/src/lean/Init/Internal.lean +%%DATADIR%%/src/lean/Init/Internal/Order.lean +%%DATADIR%%/src/lean/Init/Internal/Order/Basic.lean +%%DATADIR%%/src/lean/Init/Internal/Order/Lemmas.lean +%%DATADIR%%/src/lean/Init/Internal/Order/Tactic.lean %%DATADIR%%/src/lean/Init/MacroTrace.lean %%DATADIR%%/src/lean/Init/Meta.lean %%DATADIR%%/src/lean/Init/MetaTypes.lean @@ -2463,6 +3941,7 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Init/Simproc.lean %%DATADIR%%/src/lean/Init/SizeOf.lean %%DATADIR%%/src/lean/Init/SizeOfLemmas.lean +%%DATADIR%%/src/lean/Init/Syntax.lean %%DATADIR%%/src/lean/Init/System.lean %%DATADIR%%/src/lean/Init/System/FilePath.lean %%DATADIR%%/src/lean/Init/System/IO.lean @@ -2474,9 +3953,12 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Init/System/Uri.lean %%DATADIR%%/src/lean/Init/Tactics.lean %%DATADIR%%/src/lean/Init/TacticsExtra.lean +%%DATADIR%%/src/lean/Init/Task.lean +%%DATADIR%%/src/lean/Init/Try.lean %%DATADIR%%/src/lean/Init/Util.lean %%DATADIR%%/src/lean/Init/WF.lean %%DATADIR%%/src/lean/Init/WFTactics.lean +%%DATADIR%%/src/lean/Init/While.lean %%DATADIR%%/src/lean/Lean.lean %%DATADIR%%/src/lean/Lean/AddDecl.lean %%DATADIR%%/src/lean/Lean/Attributes.lean @@ -2538,7 +4020,6 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Compiler/LCNF/FVarUtil.lean %%DATADIR%%/src/lean/Lean/Compiler/LCNF/FixedParams.lean %%DATADIR%%/src/lean/Lean/Compiler/LCNF/FloatLetIn.lean -%%DATADIR%%/src/lean/Lean/Compiler/LCNF/ForEachExpr.lean %%DATADIR%%/src/lean/Lean/Compiler/LCNF/InferType.lean %%DATADIR%%/src/lean/Lean/Compiler/LCNF/Internalize.lean %%DATADIR%%/src/lean/Lean/Compiler/LCNF/JoinPoints.lean @@ -2594,10 +4075,9 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Data.lean %%DATADIR%%/src/lean/Lean/Data/Array.lean %%DATADIR%%/src/lean/Lean/Data/AssocList.lean +%%DATADIR%%/src/lean/Lean/Data/DeclarationRange.lean %%DATADIR%%/src/lean/Lean/Data/Format.lean %%DATADIR%%/src/lean/Lean/Data/FuzzyMatching.lean -%%DATADIR%%/src/lean/Lean/Data/HashMap.lean -%%DATADIR%%/src/lean/Lean/Data/HashSet.lean %%DATADIR%%/src/lean/Lean/Data/Json.lean %%DATADIR%%/src/lean/Lean/Data/Json/Basic.lean %%DATADIR%%/src/lean/Lean/Data/Json/Elab.lean @@ -2611,6 +4091,7 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Data/LOption.lean %%DATADIR%%/src/lean/Lean/Data/Lsp.lean %%DATADIR%%/src/lean/Lean/Data/Lsp/Basic.lean +%%DATADIR%%/src/lean/Lean/Data/Lsp/CancelParams.lean %%DATADIR%%/src/lean/Lean/Data/Lsp/Capabilities.lean %%DATADIR%%/src/lean/Lean/Data/Lsp/Client.lean %%DATADIR%%/src/lean/Lean/Data/Lsp/CodeActions.lean @@ -2635,9 +4116,9 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Data/PersistentHashSet.lean %%DATADIR%%/src/lean/Lean/Data/Position.lean %%DATADIR%%/src/lean/Lean/Data/PrefixTree.lean +%%DATADIR%%/src/lean/Lean/Data/RArray.lean %%DATADIR%%/src/lean/Lean/Data/RBMap.lean %%DATADIR%%/src/lean/Lean/Data/RBTree.lean -%%DATADIR%%/src/lean/Lean/Data/Rat.lean %%DATADIR%%/src/lean/Lean/Data/SMap.lean %%DATADIR%%/src/lean/Lean/Data/SSet.lean %%DATADIR%%/src/lean/Lean/Data/Trie.lean @@ -2647,7 +4128,9 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Declaration.lean %%DATADIR%%/src/lean/Lean/DeclarationRange.lean %%DATADIR%%/src/lean/Lean/DocString.lean +%%DATADIR%%/src/lean/Lean/DocString/Add.lean %%DATADIR%%/src/lean/Lean/DocString/Extension.lean +%%DATADIR%%/src/lean/Lean/DocString/Links.lean %%DATADIR%%/src/lean/Lean/Elab.lean %%DATADIR%%/src/lean/Lean/Elab/App.lean %%DATADIR%%/src/lean/Lean/Elab/Arg.lean @@ -2658,6 +4141,7 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Elab/Binders.lean %%DATADIR%%/src/lean/Lean/Elab/BindersUtil.lean %%DATADIR%%/src/lean/Lean/Elab/BuiltinCommand.lean +%%DATADIR%%/src/lean/Lean/Elab/BuiltinEvalCommand.lean %%DATADIR%%/src/lean/Lean/Elab/BuiltinNotation.lean %%DATADIR%%/src/lean/Lean/Elab/BuiltinTerm.lean %%DATADIR%%/src/lean/Lean/Elab/Calc.lean @@ -2682,6 +4166,7 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Elab/Deriving/Ord.lean %%DATADIR%%/src/lean/Lean/Elab/Deriving/Repr.lean %%DATADIR%%/src/lean/Lean/Elab/Deriving/SizeOf.lean +%%DATADIR%%/src/lean/Lean/Elab/Deriving/ToExpr.lean %%DATADIR%%/src/lean/Lean/Elab/Deriving/TypeName.lean %%DATADIR%%/src/lean/Lean/Elab/Deriving/Util.lean %%DATADIR%%/src/lean/Lean/Elab/Do.lean @@ -2695,8 +4180,10 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Elab/Import.lean %%DATADIR%%/src/lean/Lean/Elab/Inductive.lean %%DATADIR%%/src/lean/Lean/Elab/InfoTree.lean +%%DATADIR%%/src/lean/Lean/Elab/InfoTree/InlayHints.lean %%DATADIR%%/src/lean/Lean/Elab/InfoTree/Main.lean %%DATADIR%%/src/lean/Lean/Elab/InfoTree/Types.lean +%%DATADIR%%/src/lean/Lean/Elab/InfoTrees.lean %%DATADIR%%/src/lean/Lean/Elab/InheritDoc.lean %%DATADIR%%/src/lean/Lean/Elab/LetRec.lean %%DATADIR%%/src/lean/Lean/Elab/Level.lean @@ -2708,6 +4195,7 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Elab/MatchExpr.lean %%DATADIR%%/src/lean/Lean/Elab/Mixfix.lean %%DATADIR%%/src/lean/Lean/Elab/MutualDef.lean +%%DATADIR%%/src/lean/Lean/Elab/MutualInductive.lean %%DATADIR%%/src/lean/Lean/Elab/Notation.lean %%DATADIR%%/src/lean/Lean/Elab/Open.lean %%DATADIR%%/src/lean/Lean/Elab/ParseImportsFast.lean @@ -2716,9 +4204,15 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/Basic.lean %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/EqUnfold.lean %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/Eqns.lean +%%DATADIR%%/src/lean/Lean/Elab/PreDefinition/FixedParams.lean %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/Main.lean %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/MkInhabitant.lean +%%DATADIR%%/src/lean/Lean/Elab/PreDefinition/Mutual.lean %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/Nonrec/Eqns.lean +%%DATADIR%%/src/lean/Lean/Elab/PreDefinition/PartialFixpoint.lean +%%DATADIR%%/src/lean/Lean/Elab/PreDefinition/PartialFixpoint/Eqns.lean +%%DATADIR%%/src/lean/Lean/Elab/PreDefinition/PartialFixpoint/Induction.lean +%%DATADIR%%/src/lean/Lean/Elab/PreDefinition/PartialFixpoint/Main.lean %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/Structural.lean %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/Structural/BRecOn.lean %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/Structural/Basic.lean @@ -2730,29 +4224,32 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/Structural/Preprocess.lean %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/Structural/RecArgInfo.lean %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/Structural/SmartUnfolding.lean -%%DATADIR%%/src/lean/Lean/Elab/PreDefinition/TerminationArgument.lean %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/TerminationHint.lean +%%DATADIR%%/src/lean/Lean/Elab/PreDefinition/TerminationMeasure.lean %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/WF.lean %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/WF/Basic.lean %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/WF/Eqns.lean %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/WF/Fix.lean +%%DATADIR%%/src/lean/Lean/Elab/PreDefinition/WF/FloatRecApp.lean %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/WF/GuessLex.lean -%%DATADIR%%/src/lean/Lean/Elab/PreDefinition/WF/Ite.lean %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/WF/Main.lean %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/WF/PackMutual.lean %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/WF/Preprocess.lean %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/WF/Rel.lean +%%DATADIR%%/src/lean/Lean/Elab/PreDefinition/WF/Unfold.lean %%DATADIR%%/src/lean/Lean/Elab/Print.lean %%DATADIR%%/src/lean/Lean/Elab/Quotation.lean %%DATADIR%%/src/lean/Lean/Elab/Quotation/Precheck.lean %%DATADIR%%/src/lean/Lean/Elab/Quotation/Util.lean %%DATADIR%%/src/lean/Lean/Elab/RecAppSyntax.lean +%%DATADIR%%/src/lean/Lean/Elab/RecommendedSpelling.lean %%DATADIR%%/src/lean/Lean/Elab/SetOption.lean %%DATADIR%%/src/lean/Lean/Elab/StructInst.lean %%DATADIR%%/src/lean/Lean/Elab/Structure.lean %%DATADIR%%/src/lean/Lean/Elab/Syntax.lean %%DATADIR%%/src/lean/Lean/Elab/SyntheticMVars.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic.lean +%%DATADIR%%/src/lean/Lean/Elab/Tactic/AsAuxLemma.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic/BVDecide.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic/BVDecide/External.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic/BVDecide/Frontend.lean @@ -2763,18 +4260,32 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVExpr.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVLogical.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVPred.lean +%%DATADIR%%/src/lean/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedLemmas.lean +%%DATADIR%%/src/lean/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reify.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/SatAtBVLogical.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic/BVDecide/Frontend/BVTrace.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic/BVDecide/Frontend/LRAT.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic/BVDecide/Frontend/Normalize.lean +%%DATADIR%%/src/lean/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/AC.lean +%%DATADIR%%/src/lean/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/AndFlatten.lean +%%DATADIR%%/src/lean/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/ApplyControlFlow.lean +%%DATADIR%%/src/lean/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Basic.lean +%%DATADIR%%/src/lean/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/EmbeddedConstraint.lean +%%DATADIR%%/src/lean/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Enums.lean +%%DATADIR%%/src/lean/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/IntToBitVec.lean +%%DATADIR%%/src/lean/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Rewrite.lean +%%DATADIR%%/src/lean/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/ShortCircuit.lean +%%DATADIR%%/src/lean/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Simproc.lean +%%DATADIR%%/src/lean/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Structures.lean +%%DATADIR%%/src/lean/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/TypeAnalysis.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic/BVDecide/LRAT.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic/BVDecide/LRAT/Trim.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic/Basic.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic/BoolToPropSimps.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic/BuiltinTactic.lean -%%DATADIR%%/src/lean/Lean/Elab/Tactic/Cache.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic/Calc.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic/Change.lean +%%DATADIR%%/src/lean/Lean/Elab/Tactic/Classical.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic/Config.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic/Congr.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic/Conv.lean @@ -2782,6 +4293,7 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Elab/Tactic/Conv/Change.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic/Conv/Congr.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic/Conv/Delta.lean +%%DATADIR%%/src/lean/Lean/Elab/Tactic/Conv/Lets.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic/Conv/Pattern.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic/Conv/Rewrite.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic/Conv/Simp.lean @@ -2790,16 +4302,20 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Elab/Tactic/DiscrTreeKey.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic/Doc.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic/ElabTerm.lean +%%DATADIR%%/src/lean/Lean/Elab/Tactic/ExposeNames.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic/Ext.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic/FalseOrByContra.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic/Generalize.lean +%%DATADIR%%/src/lean/Lean/Elab/Tactic/Grind.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic/Guard.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic/Induction.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic/Injection.lean +%%DATADIR%%/src/lean/Lean/Elab/Tactic/Lets.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic/LibrarySearch.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic/Location.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic/Match.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic/Meta.lean +%%DATADIR%%/src/lean/Lean/Elab/Tactic/Monotonicity.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic/NormCast.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic/Omega.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic/Omega/Core.lean @@ -2813,18 +4329,21 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Elab/Tactic/Rfl.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic/ShowTerm.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic/Simp.lean +%%DATADIR%%/src/lean/Lean/Elab/Tactic/SimpArith.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic/SimpTrace.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic/Simpa.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic/Simproc.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic/SolveByElim.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic/Split.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic/Symm.lean +%%DATADIR%%/src/lean/Lean/Elab/Tactic/TreeTacAttr.lean +%%DATADIR%%/src/lean/Lean/Elab/Tactic/Try.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic/Unfold.lean %%DATADIR%%/src/lean/Lean/Elab/Term.lean %%DATADIR%%/src/lean/Lean/Elab/Time.lean %%DATADIR%%/src/lean/Lean/Elab/Util.lean +%%DATADIR%%/src/lean/Lean/EnvExtension.lean %%DATADIR%%/src/lean/Lean/Environment.lean -%%DATADIR%%/src/lean/Lean/Eval.lean %%DATADIR%%/src/lean/Lean/Exception.lean %%DATADIR%%/src/lean/Lean/Expr.lean %%DATADIR%%/src/lean/Lean/HeadIndex.lean @@ -2836,13 +4355,14 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Language/Basic.lean %%DATADIR%%/src/lean/Lean/Language/Lean.lean %%DATADIR%%/src/lean/Lean/Language/Lean/Types.lean -%%DATADIR%%/src/lean/Lean/LazyInitExtension.lean +%%DATADIR%%/src/lean/Lean/Language/Util.lean %%DATADIR%%/src/lean/Lean/Level.lean %%DATADIR%%/src/lean/Lean/Linter.lean %%DATADIR%%/src/lean/Lean/Linter/Basic.lean %%DATADIR%%/src/lean/Lean/Linter/Builtin.lean %%DATADIR%%/src/lean/Lean/Linter/ConstructorAsVariable.lean %%DATADIR%%/src/lean/Lean/Linter/Deprecated.lean +%%DATADIR%%/src/lean/Lean/Linter/List.lean %%DATADIR%%/src/lean/Lean/Linter/MissingDocs.lean %%DATADIR%%/src/lean/Lean/Linter/Omit.lean %%DATADIR%%/src/lean/Lean/Linter/UnusedVariables.lean @@ -2859,6 +4379,7 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Meta/ArgsPacker.lean %%DATADIR%%/src/lean/Lean/Meta/ArgsPacker/Basic.lean %%DATADIR%%/src/lean/Lean/Meta/Basic.lean +%%DATADIR%%/src/lean/Lean/Meta/BinderNameHint.lean %%DATADIR%%/src/lean/Lean/Meta/Canonicalizer.lean %%DATADIR%%/src/lean/Lean/Meta/Check.lean %%DATADIR%%/src/lean/Lean/Meta/CheckTactic.lean @@ -2895,6 +4416,7 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Meta/InferType.lean %%DATADIR%%/src/lean/Lean/Meta/Injective.lean %%DATADIR%%/src/lean/Lean/Meta/Instances.lean +%%DATADIR%%/src/lean/Lean/Meta/IntInstTesters.lean %%DATADIR%%/src/lean/Lean/Meta/Iterator.lean %%DATADIR%%/src/lean/Lean/Meta/KAbstract.lean %%DATADIR%%/src/lean/Lean/Meta/KExprMap.lean @@ -2918,12 +4440,14 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Meta/MatchUtil.lean %%DATADIR%%/src/lean/Lean/Meta/NatInstTesters.lean %%DATADIR%%/src/lean/Lean/Meta/Offset.lean +%%DATADIR%%/src/lean/Lean/Meta/Order.lean %%DATADIR%%/src/lean/Lean/Meta/PPGoal.lean %%DATADIR%%/src/lean/Lean/Meta/PProdN.lean %%DATADIR%%/src/lean/Lean/Meta/RecursorInfo.lean %%DATADIR%%/src/lean/Lean/Meta/Reduce.lean %%DATADIR%%/src/lean/Lean/Meta/ReduceEval.lean %%DATADIR%%/src/lean/Lean/Meta/SizeOf.lean +%%DATADIR%%/src/lean/Lean/Meta/Sorry.lean %%DATADIR%%/src/lean/Lean/Meta/Structure.lean %%DATADIR%%/src/lean/Lean/Meta/SynthInstance.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic.lean @@ -2943,32 +4467,103 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Meta/Tactic/Contradiction.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Delta.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/ElimInfo.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/ExposeNames.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Ext.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/FVarSubst.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/FunInd.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/FunIndCollect.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/FunIndInfo.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Generalize.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/CommRing.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/DenoteExpr.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/EqCnstr.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Internalize.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Inv.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Poly.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Proof.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Reify.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/RingId.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/ToExpr.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Types.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Util.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Var.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/DvdCnstr.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/Foreign.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/Inv.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/LeCnstr.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/MBTC.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/Model.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/Nat.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/Norm.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/Search.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/SearchM.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/Types.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/Util.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/Cutsat/Var.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/Internalize.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/Inv.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/Main.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/Model.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/Offset.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/Offset/Main.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/Offset/Model.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/Offset/Proof.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/Offset/Types.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/Offset/Util.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/ProofUtil.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/Types.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Arith/Util.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Attr.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Beta.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Canon.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Cases.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/CasesMatch.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Combinators.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Core.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Ctor.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Diseq.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/EMatch.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/EMatchTheorem.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/ENodeKey.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/EqResolution.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Ext.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/ExtAttr.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/ForallProp.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Injection.lean -%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Preprocessor.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Internalize.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Intro.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Inv.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Lookahead.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/MBTC.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Main.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/MarkNestedProofs.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/MatchCond.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/MatchDiscrOnly.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/PP.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Parser.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Proj.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Proof.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Propagate.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/PropagatorAttr.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/ProveEq.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/RevertAll.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Simp.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/SimpUtil.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Solve.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Split.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Types.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Util.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/IndependentOf.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Induction.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Injection.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Intro.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Lets.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/LibrarySearch.lean -%%DATADIR%%/src/lean/Lean/Meta/Tactic/LinearArith.lean -%%DATADIR%%/src/lean/Lean/Meta/Tactic/LinearArith/Basic.lean -%%DATADIR%%/src/lean/Lean/Meta/Tactic/LinearArith/Main.lean -%%DATADIR%%/src/lean/Lean/Meta/Tactic/LinearArith/Nat.lean -%%DATADIR%%/src/lean/Lean/Meta/Tactic/LinearArith/Nat/Basic.lean -%%DATADIR%%/src/lean/Lean/Meta/Tactic/LinearArith/Nat/Simp.lean -%%DATADIR%%/src/lean/Lean/Meta/Tactic/LinearArith/Nat/Solver.lean -%%DATADIR%%/src/lean/Lean/Meta/Tactic/LinearArith/Simp.lean -%%DATADIR%%/src/lean/Lean/Meta/Tactic/LinearArith/Solver.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/NormCast.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Refl.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Rename.lean @@ -2979,6 +4574,14 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Meta/Tactic/Rewrites.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Rfl.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/Arith.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/Arith/Int.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/Arith/Int/Basic.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/Arith/Int/Simp.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/Arith/Nat.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/Arith/Nat/Basic.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/Arith/Nat/Simp.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/Arith/Util.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/Attr.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Array.lean @@ -2989,6 +4592,7 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Int.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/List.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/SInt.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/String.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/UInt.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Util.lean @@ -3006,6 +4610,8 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Meta/Tactic/SplitIf.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Subst.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Symm.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Try.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Try/Collect.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/TryThis.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Unfold.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/UnifyEq.lean @@ -3017,6 +4623,7 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/MetavarContext.lean %%DATADIR%%/src/lean/Lean/Modifiers.lean %%DATADIR%%/src/lean/Lean/MonadEnv.lean +%%DATADIR%%/src/lean/Lean/Namespace.lean %%DATADIR%%/src/lean/Lean/Parser.lean %%DATADIR%%/src/lean/Lean/Parser/Attr.lean %%DATADIR%%/src/lean/Lean/Parser/Basic.lean @@ -3031,9 +4638,11 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Parser/Tactic.lean %%DATADIR%%/src/lean/Lean/Parser/Tactic/Doc.lean %%DATADIR%%/src/lean/Lean/Parser/Term.lean +%%DATADIR%%/src/lean/Lean/Parser/Term/Doc.lean %%DATADIR%%/src/lean/Lean/Parser/Types.lean %%DATADIR%%/src/lean/Lean/ParserCompiler.lean %%DATADIR%%/src/lean/Lean/ParserCompiler/Attribute.lean +%%DATADIR%%/src/lean/Lean/PremiseSelection.lean %%DATADIR%%/src/lean/Lean/PrettyPrinter.lean %%DATADIR%%/src/lean/Lean/PrettyPrinter/Basic.lean %%DATADIR%%/src/lean/Lean/PrettyPrinter/Delaborator.lean @@ -3046,6 +4655,7 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean %%DATADIR%%/src/lean/Lean/PrettyPrinter/Formatter.lean %%DATADIR%%/src/lean/Lean/PrettyPrinter/Parenthesizer.lean +%%DATADIR%%/src/lean/Lean/PrivateName.lean %%DATADIR%%/src/lean/Lean/ProjFns.lean %%DATADIR%%/src/lean/Lean/ReducibilityAttrs.lean %%DATADIR%%/src/lean/Lean/Replay.lean @@ -3059,37 +4669,55 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Server/CodeActions/Attr.lean %%DATADIR%%/src/lean/Lean/Server/CodeActions/Basic.lean %%DATADIR%%/src/lean/Lean/Server/CodeActions/Provider.lean +%%DATADIR%%/src/lean/Lean/Server/CodeActions/UnknownIdentifier.lean %%DATADIR%%/src/lean/Lean/Server/Completion.lean -%%DATADIR%%/src/lean/Lean/Server/CompletionItemData.lean +%%DATADIR%%/src/lean/Lean/Server/Completion/CompletionCollectors.lean +%%DATADIR%%/src/lean/Lean/Server/Completion/CompletionInfoSelection.lean +%%DATADIR%%/src/lean/Lean/Server/Completion/CompletionItemData.lean +%%DATADIR%%/src/lean/Lean/Server/Completion/CompletionResolution.lean +%%DATADIR%%/src/lean/Lean/Server/Completion/CompletionUtils.lean +%%DATADIR%%/src/lean/Lean/Server/Completion/EligibleHeaderDecls.lean +%%DATADIR%%/src/lean/Lean/Server/Completion/ImportCompletion.lean +%%DATADIR%%/src/lean/Lean/Server/Completion/SyntheticCompletion.lean %%DATADIR%%/src/lean/Lean/Server/FileSource.lean %%DATADIR%%/src/lean/Lean/Server/FileWorker.lean +%%DATADIR%%/src/lean/Lean/Server/FileWorker/ExampleHover.lean +%%DATADIR%%/src/lean/Lean/Server/FileWorker/InlayHints.lean %%DATADIR%%/src/lean/Lean/Server/FileWorker/RequestHandling.lean +%%DATADIR%%/src/lean/Lean/Server/FileWorker/SemanticHighlighting.lean %%DATADIR%%/src/lean/Lean/Server/FileWorker/SetupFile.lean %%DATADIR%%/src/lean/Lean/Server/FileWorker/Utils.lean %%DATADIR%%/src/lean/Lean/Server/FileWorker/WidgetRequests.lean %%DATADIR%%/src/lean/Lean/Server/GoTo.lean -%%DATADIR%%/src/lean/Lean/Server/ImportCompletion.lean %%DATADIR%%/src/lean/Lean/Server/InfoUtils.lean %%DATADIR%%/src/lean/Lean/Server/README.md %%DATADIR%%/src/lean/Lean/Server/References.lean +%%DATADIR%%/src/lean/Lean/Server/RequestCancellation.lean %%DATADIR%%/src/lean/Lean/Server/Requests.lean %%DATADIR%%/src/lean/Lean/Server/Rpc.lean %%DATADIR%%/src/lean/Lean/Server/Rpc/Basic.lean %%DATADIR%%/src/lean/Lean/Server/Rpc/Deriving.lean %%DATADIR%%/src/lean/Lean/Server/Rpc/RequestHandling.lean +%%DATADIR%%/src/lean/Lean/Server/ServerTask.lean %%DATADIR%%/src/lean/Lean/Server/Snapshots.lean +%%DATADIR%%/src/lean/Lean/Server/Test.lean +%%DATADIR%%/src/lean/Lean/Server/Test/Cancel.lean +%%DATADIR%%/src/lean/Lean/Server/Test/Runner.lean %%DATADIR%%/src/lean/Lean/Server/Utils.lean %%DATADIR%%/src/lean/Lean/Server/Watchdog.lean %%DATADIR%%/src/lean/Lean/Structure.lean %%DATADIR%%/src/lean/Lean/SubExpr.lean %%DATADIR%%/src/lean/Lean/Syntax.lean %%DATADIR%%/src/lean/Lean/ToExpr.lean +%%DATADIR%%/src/lean/Lean/ToLevel.lean %%DATADIR%%/src/lean/Lean/Util.lean %%DATADIR%%/src/lean/Lean/Util/CollectAxioms.lean %%DATADIR%%/src/lean/Lean/Util/CollectFVars.lean +%%DATADIR%%/src/lean/Lean/Util/CollectLevelMVars.lean %%DATADIR%%/src/lean/Lean/Util/CollectLevelParams.lean %%DATADIR%%/src/lean/Lean/Util/CollectMVars.lean %%DATADIR%%/src/lean/Lean/Util/Diff.lean +%%DATADIR%%/src/lean/Lean/Util/FVarSubset.lean %%DATADIR%%/src/lean/Lean/Util/FileSetupInfo.lean %%DATADIR%%/src/lean/Lean/Util/FindExpr.lean %%DATADIR%%/src/lean/Lean/Util/FindLevelMVar.lean @@ -3122,6 +4750,7 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Util/SearchPath.lean %%DATADIR%%/src/lean/Lean/Util/ShareCommon.lean %%DATADIR%%/src/lean/Lean/Util/Sorry.lean +%%DATADIR%%/src/lean/Lean/Util/SortExprs.lean %%DATADIR%%/src/lean/Lean/Util/TestExtern.lean %%DATADIR%%/src/lean/Lean/Util/Trace.lean %%DATADIR%%/src/lean/Lean/Widget.lean @@ -3135,6 +4764,8 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Widget/UserWidget.lean %%DATADIR%%/src/lean/Leanc.lean %%DATADIR%%/src/lean/Std.lean +%%DATADIR%%/src/lean/Std/Classes.lean +%%DATADIR%%/src/lean/Std/Classes/Ord.lean %%DATADIR%%/src/lean/Std/Data.lean %%DATADIR%%/src/lean/Std/Data/DHashMap.lean %%DATADIR%%/src/lean/Std/Data/DHashMap/AdditionalOperations.lean @@ -3142,12 +4773,8 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Std/Data/DHashMap/Internal/AssocList/Basic.lean %%DATADIR%%/src/lean/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean %%DATADIR%%/src/lean/Std/Data/DHashMap/Internal/Defs.lean +%%DATADIR%%/src/lean/Std/Data/DHashMap/Internal/HashesTo.lean %%DATADIR%%/src/lean/Std/Data/DHashMap/Internal/Index.lean -%%DATADIR%%/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean -%%DATADIR%%/src/lean/Std/Data/DHashMap/Internal/List/Defs.lean -%%DATADIR%%/src/lean/Std/Data/DHashMap/Internal/List/HashesTo.lean -%%DATADIR%%/src/lean/Std/Data/DHashMap/Internal/List/Pairwise.lean -%%DATADIR%%/src/lean/Std/Data/DHashMap/Internal/List/Sublist.lean %%DATADIR%%/src/lean/Std/Data/DHashMap/Internal/Model.lean %%DATADIR%%/src/lean/Std/Data/DHashMap/Internal/Raw.lean %%DATADIR%%/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean @@ -3156,6 +4783,35 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Std/Data/DHashMap/Raw.lean %%DATADIR%%/src/lean/Std/Data/DHashMap/RawDef.lean %%DATADIR%%/src/lean/Std/Data/DHashMap/RawLemmas.lean +%%DATADIR%%/src/lean/Std/Data/DTreeMap.lean +%%DATADIR%%/src/lean/Std/Data/DTreeMap/AdditionalOperations.lean +%%DATADIR%%/src/lean/Std/Data/DTreeMap/Basic.lean +%%DATADIR%%/src/lean/Std/Data/DTreeMap/Internal/Balanced.lean +%%DATADIR%%/src/lean/Std/Data/DTreeMap/Internal/Balancing.lean +%%DATADIR%%/src/lean/Std/Data/DTreeMap/Internal/Cell.lean +%%DATADIR%%/src/lean/Std/Data/DTreeMap/Internal/Def.lean +%%DATADIR%%/src/lean/Std/Data/DTreeMap/Internal/Lemmas.lean +%%DATADIR%%/src/lean/Std/Data/DTreeMap/Internal/Model.lean +%%DATADIR%%/src/lean/Std/Data/DTreeMap/Internal/Operations.lean +%%DATADIR%%/src/lean/Std/Data/DTreeMap/Internal/Ordered.lean +%%DATADIR%%/src/lean/Std/Data/DTreeMap/Internal/Queries.lean +%%DATADIR%%/src/lean/Std/Data/DTreeMap/Internal/WF/Defs.lean +%%DATADIR%%/src/lean/Std/Data/DTreeMap/Internal/WF/Lemmas.lean +%%DATADIR%%/src/lean/Std/Data/DTreeMap/Lemmas.lean +%%DATADIR%%/src/lean/Std/Data/DTreeMap/Raw.lean +%%DATADIR%%/src/lean/Std/Data/DTreeMap/Raw/AdditionalOperations.lean +%%DATADIR%%/src/lean/Std/Data/DTreeMap/Raw/Basic.lean +%%DATADIR%%/src/lean/Std/Data/DTreeMap/Raw/Lemmas.lean +%%DATADIR%%/src/lean/Std/Data/DTreeMap/Raw/WF.lean +%%DATADIR%%/src/lean/Std/Data/ExtDHashMap.lean +%%DATADIR%%/src/lean/Std/Data/ExtDHashMap/Basic.lean +%%DATADIR%%/src/lean/Std/Data/ExtDHashMap/Lemmas.lean +%%DATADIR%%/src/lean/Std/Data/ExtHashMap.lean +%%DATADIR%%/src/lean/Std/Data/ExtHashMap/Basic.lean +%%DATADIR%%/src/lean/Std/Data/ExtHashMap/Lemmas.lean +%%DATADIR%%/src/lean/Std/Data/ExtHashSet.lean +%%DATADIR%%/src/lean/Std/Data/ExtHashSet/Basic.lean +%%DATADIR%%/src/lean/Std/Data/ExtHashSet/Lemmas.lean %%DATADIR%%/src/lean/Std/Data/HashMap.lean %%DATADIR%%/src/lean/Std/Data/HashMap/AdditionalOperations.lean %%DATADIR%%/src/lean/Std/Data/HashMap/Basic.lean @@ -3167,11 +4823,45 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Std/Data/HashSet/Lemmas.lean %%DATADIR%%/src/lean/Std/Data/HashSet/Raw.lean %%DATADIR%%/src/lean/Std/Data/HashSet/RawLemmas.lean +%%DATADIR%%/src/lean/Std/Data/Internal/Cut.lean +%%DATADIR%%/src/lean/Std/Data/Internal/List/Associative.lean +%%DATADIR%%/src/lean/Std/Data/Internal/List/Defs.lean +%%DATADIR%%/src/lean/Std/Data/TreeMap.lean +%%DATADIR%%/src/lean/Std/Data/TreeMap/AdditionalOperations.lean +%%DATADIR%%/src/lean/Std/Data/TreeMap/Basic.lean +%%DATADIR%%/src/lean/Std/Data/TreeMap/Lemmas.lean +%%DATADIR%%/src/lean/Std/Data/TreeMap/Raw.lean +%%DATADIR%%/src/lean/Std/Data/TreeMap/Raw/AdditionalOperations.lean +%%DATADIR%%/src/lean/Std/Data/TreeMap/Raw/Basic.lean +%%DATADIR%%/src/lean/Std/Data/TreeMap/Raw/Lemmas.lean +%%DATADIR%%/src/lean/Std/Data/TreeMap/Raw/WF.lean +%%DATADIR%%/src/lean/Std/Data/TreeSet.lean +%%DATADIR%%/src/lean/Std/Data/TreeSet/AdditionalOperations.lean +%%DATADIR%%/src/lean/Std/Data/TreeSet/Basic.lean +%%DATADIR%%/src/lean/Std/Data/TreeSet/Lemmas.lean +%%DATADIR%%/src/lean/Std/Data/TreeSet/Raw.lean +%%DATADIR%%/src/lean/Std/Data/TreeSet/Raw/Basic.lean +%%DATADIR%%/src/lean/Std/Data/TreeSet/Raw/Lemmas.lean +%%DATADIR%%/src/lean/Std/Data/TreeSet/Raw/WF.lean %%DATADIR%%/src/lean/Std/Internal.lean +%%DATADIR%%/src/lean/Std/Internal/Async.lean +%%DATADIR%%/src/lean/Std/Internal/Async/Basic.lean +%%DATADIR%%/src/lean/Std/Internal/Async/Select.lean +%%DATADIR%%/src/lean/Std/Internal/Async/TCP.lean +%%DATADIR%%/src/lean/Std/Internal/Async/Timer.lean +%%DATADIR%%/src/lean/Std/Internal/Async/UDP.lean %%DATADIR%%/src/lean/Std/Internal/Parsec.lean %%DATADIR%%/src/lean/Std/Internal/Parsec/Basic.lean %%DATADIR%%/src/lean/Std/Internal/Parsec/ByteArray.lean %%DATADIR%%/src/lean/Std/Internal/Parsec/String.lean +%%DATADIR%%/src/lean/Std/Internal/Rat.lean +%%DATADIR%%/src/lean/Std/Internal/UV.lean +%%DATADIR%%/src/lean/Std/Internal/UV/Loop.lean +%%DATADIR%%/src/lean/Std/Internal/UV/TCP.lean +%%DATADIR%%/src/lean/Std/Internal/UV/Timer.lean +%%DATADIR%%/src/lean/Std/Internal/UV/UDP.lean +%%DATADIR%%/src/lean/Std/Net.lean +%%DATADIR%%/src/lean/Std/Net/Addr.lean %%DATADIR%%/src/lean/Std/Sat.lean %%DATADIR%%/src/lean/Std/Sat/AIG.lean %%DATADIR%%/src/lean/Std/Sat/AIG/Basic.lean @@ -3197,6 +4887,13 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Std/Sat/CNF/Literal.lean %%DATADIR%%/src/lean/Std/Sat/CNF/Relabel.lean %%DATADIR%%/src/lean/Std/Sat/CNF/RelabelFin.lean +%%DATADIR%%/src/lean/Std/Sync.lean +%%DATADIR%%/src/lean/Std/Sync/Barrier.lean +%%DATADIR%%/src/lean/Std/Sync/Basic.lean +%%DATADIR%%/src/lean/Std/Sync/Channel.lean +%%DATADIR%%/src/lean/Std/Sync/Mutex.lean +%%DATADIR%%/src/lean/Std/Sync/RecursiveMutex.lean +%%DATADIR%%/src/lean/Std/Sync/SharedMutex.lean %%DATADIR%%/src/lean/Std/Tactic.lean %%DATADIR%%/src/lean/Std/Tactic/BVDecide.lean %%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast.lean @@ -3207,54 +4904,57 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Carry.lean %%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Const.lean %%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Expr.lean -%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations.lean %%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Add.lean %%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Append.lean %%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Eq.lean %%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Extract.lean %%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/GetLsbD.lean %%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Mul.lean +%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Neg.lean %%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Not.lean %%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Replicate.lean %%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/RotateLeft.lean %%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/RotateRight.lean %%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/ShiftLeft.lean %%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/ShiftRight.lean -%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/SignExtend.lean +%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Sub.lean +%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Udiv.lean %%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Ult.lean +%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Umod.lean %%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/ZeroExtend.lean %%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Pred.lean +%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Substructure.lean %%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Var.lean %%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas.lean %%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Basic.lean %%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Carry.lean %%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Const.lean %%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean -%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations.lean %%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Add.lean %%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Append.lean %%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Eq.lean %%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Extract.lean %%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/GetLsbD.lean %%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Mul.lean +%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Neg.lean %%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Not.lean %%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Replicate.lean %%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/RotateLeft.lean %%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/RotateRight.lean %%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftLeft.lean %%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftRight.lean -%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/SignExtend.lean +%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Sub.lean +%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Udiv.lean %%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Ult.lean +%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Umod.lean %%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ZeroExtend.lean %%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Pred.lean %%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Var.lean %%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BoolExpr.lean %%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BoolExpr/Basic.lean -%%DATADIR%%/src/lean/Std/Tactic/BVDecide/Bitblast/BoolExpr/Circuit.lean %%DATADIR%%/src/lean/Std/Tactic/BVDecide/LRAT.lean %%DATADIR%%/src/lean/Std/Tactic/BVDecide/LRAT/Actions.lean %%DATADIR%%/src/lean/Std/Tactic/BVDecide/LRAT/Checker.lean -%%DATADIR%%/src/lean/Std/Tactic/BVDecide/LRAT/Internal.lean %%DATADIR%%/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Actions.lean %%DATADIR%%/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Assignment.lean %%DATADIR%%/src/lean/Std/Tactic/BVDecide/LRAT/Internal/CNF.lean @@ -3282,25 +4982,78 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Std/Tactic/BVDecide/Normalize/Prop.lean %%DATADIR%%/src/lean/Std/Tactic/BVDecide/Reflect.lean %%DATADIR%%/src/lean/Std/Tactic/BVDecide/Syntax.lean +%%DATADIR%%/src/lean/Std/Time.lean +%%DATADIR%%/src/lean/Std/Time/Date.lean +%%DATADIR%%/src/lean/Std/Time/Date/Basic.lean +%%DATADIR%%/src/lean/Std/Time/Date/PlainDate.lean +%%DATADIR%%/src/lean/Std/Time/Date/Unit/Basic.lean +%%DATADIR%%/src/lean/Std/Time/Date/Unit/Day.lean +%%DATADIR%%/src/lean/Std/Time/Date/Unit/Month.lean +%%DATADIR%%/src/lean/Std/Time/Date/Unit/Week.lean +%%DATADIR%%/src/lean/Std/Time/Date/Unit/Weekday.lean +%%DATADIR%%/src/lean/Std/Time/Date/Unit/Year.lean +%%DATADIR%%/src/lean/Std/Time/Date/ValidDate.lean +%%DATADIR%%/src/lean/Std/Time/DateTime.lean +%%DATADIR%%/src/lean/Std/Time/DateTime/PlainDateTime.lean +%%DATADIR%%/src/lean/Std/Time/DateTime/Timestamp.lean +%%DATADIR%%/src/lean/Std/Time/Duration.lean +%%DATADIR%%/src/lean/Std/Time/Format.lean +%%DATADIR%%/src/lean/Std/Time/Format/Basic.lean +%%DATADIR%%/src/lean/Std/Time/Internal.lean +%%DATADIR%%/src/lean/Std/Time/Internal/Bounded.lean +%%DATADIR%%/src/lean/Std/Time/Internal/UnitVal.lean +%%DATADIR%%/src/lean/Std/Time/Notation.lean +%%DATADIR%%/src/lean/Std/Time/Notation/Spec.lean +%%DATADIR%%/src/lean/Std/Time/Time.lean +%%DATADIR%%/src/lean/Std/Time/Time/Basic.lean +%%DATADIR%%/src/lean/Std/Time/Time/HourMarker.lean +%%DATADIR%%/src/lean/Std/Time/Time/PlainTime.lean +%%DATADIR%%/src/lean/Std/Time/Time/Unit/Basic.lean +%%DATADIR%%/src/lean/Std/Time/Time/Unit/Hour.lean +%%DATADIR%%/src/lean/Std/Time/Time/Unit/Millisecond.lean +%%DATADIR%%/src/lean/Std/Time/Time/Unit/Minute.lean +%%DATADIR%%/src/lean/Std/Time/Time/Unit/Nanosecond.lean +%%DATADIR%%/src/lean/Std/Time/Time/Unit/Second.lean +%%DATADIR%%/src/lean/Std/Time/Zoned.lean +%%DATADIR%%/src/lean/Std/Time/Zoned/Database.lean +%%DATADIR%%/src/lean/Std/Time/Zoned/Database/Basic.lean +%%DATADIR%%/src/lean/Std/Time/Zoned/Database/TZdb.lean +%%DATADIR%%/src/lean/Std/Time/Zoned/Database/TzIf.lean +%%DATADIR%%/src/lean/Std/Time/Zoned/Database/Windows.lean +%%DATADIR%%/src/lean/Std/Time/Zoned/DateTime.lean +%%DATADIR%%/src/lean/Std/Time/Zoned/Offset.lean +%%DATADIR%%/src/lean/Std/Time/Zoned/TimeZone.lean +%%DATADIR%%/src/lean/Std/Time/Zoned/ZoneRules.lean +%%DATADIR%%/src/lean/Std/Time/Zoned/ZonedDateTime.lean +%%DATADIR%%/src/lean/cmake/Modules/README.md %%DATADIR%%/src/lean/lake/Lake.lean %%DATADIR%%/src/lean/lake/Lake/Build.lean %%DATADIR%%/src/lean/lake/Lake/Build/Actions.lean -%%DATADIR%%/src/lean/lake/Lake/Build/Basic.lean %%DATADIR%%/src/lean/lake/Lake/Build/Common.lean +%%DATADIR%%/src/lean/lake/Lake/Build/Context.lean %%DATADIR%%/src/lean/lake/Lake/Build/Data.lean %%DATADIR%%/src/lean/lake/Lake/Build/Executable.lean +%%DATADIR%%/src/lean/lake/Lake/Build/ExternLib.lean %%DATADIR%%/src/lean/lake/Lake/Build/Facets.lean %%DATADIR%%/src/lean/lake/Lake/Build/Fetch.lean %%DATADIR%%/src/lean/lake/Lake/Build/Imports.lean %%DATADIR%%/src/lean/lake/Lake/Build/Index.lean %%DATADIR%%/src/lean/lake/Lake/Build/Info.lean +%%DATADIR%%/src/lean/lake/Lake/Build/InitFacets.lean +%%DATADIR%%/src/lean/lake/Lake/Build/InputFile.lean %%DATADIR%%/src/lean/lake/Lake/Build/Job.lean +%%DATADIR%%/src/lean/lake/Lake/Build/Job/Basic.lean +%%DATADIR%%/src/lean/lake/Lake/Build/Job/Monad.lean +%%DATADIR%%/src/lean/lake/Lake/Build/Job/Register.lean %%DATADIR%%/src/lean/lake/Lake/Build/Key.lean %%DATADIR%%/src/lean/lake/Lake/Build/Library.lean %%DATADIR%%/src/lean/lake/Lake/Build/Module.lean %%DATADIR%%/src/lean/lake/Lake/Build/Package.lean %%DATADIR%%/src/lean/lake/Lake/Build/Run.lean %%DATADIR%%/src/lean/lake/Lake/Build/Store.lean +%%DATADIR%%/src/lean/lake/Lake/Build/Target.lean +%%DATADIR%%/src/lean/lake/Lake/Build/Target/Basic.lean +%%DATADIR%%/src/lean/lake/Lake/Build/Target/Fetch.lean %%DATADIR%%/src/lean/lake/Lake/Build/Targets.lean %%DATADIR%%/src/lean/lake/Lake/Build/Topological.lean %%DATADIR%%/src/lean/lake/Lake/Build/Trace.lean @@ -3316,25 +5069,34 @@ share/lean/lean.mk %%DATADIR%%/src/lean/lake/Lake/CLI/Translate/Lean.lean %%DATADIR%%/src/lean/lake/Lake/CLI/Translate/Toml.lean %%DATADIR%%/src/lean/lake/Lake/Config.lean +%%DATADIR%%/src/lean/lake/Lake/Config/ConfigDecl.lean +%%DATADIR%%/src/lean/lake/Lake/Config/ConfigTarget.lean %%DATADIR%%/src/lean/lake/Lake/Config/Context.lean %%DATADIR%%/src/lean/lake/Lake/Config/Defaults.lean %%DATADIR%%/src/lean/lake/Lake/Config/Dependency.lean +%%DATADIR%%/src/lean/lake/Lake/Config/Dynlib.lean %%DATADIR%%/src/lean/lake/Lake/Config/Env.lean %%DATADIR%%/src/lean/lake/Lake/Config/ExternLib.lean %%DATADIR%%/src/lean/lake/Lake/Config/ExternLibConfig.lean %%DATADIR%%/src/lean/lake/Lake/Config/FacetConfig.lean %%DATADIR%%/src/lean/lake/Lake/Config/Glob.lean +%%DATADIR%%/src/lean/lake/Lake/Config/InputFile.lean +%%DATADIR%%/src/lean/lake/Lake/Config/InputFileConfig.lean %%DATADIR%%/src/lean/lake/Lake/Config/InstallPath.lean +%%DATADIR%%/src/lean/lake/Lake/Config/Kinds.lean %%DATADIR%%/src/lean/lake/Lake/Config/Lang.lean %%DATADIR%%/src/lean/lake/Lake/Config/LeanConfig.lean %%DATADIR%%/src/lean/lake/Lake/Config/LeanExe.lean %%DATADIR%%/src/lean/lake/Lake/Config/LeanExeConfig.lean %%DATADIR%%/src/lean/lake/Lake/Config/LeanLib.lean %%DATADIR%%/src/lean/lake/Lake/Config/LeanLibConfig.lean +%%DATADIR%%/src/lean/lake/Lake/Config/Meta.lean %%DATADIR%%/src/lean/lake/Lake/Config/Module.lean %%DATADIR%%/src/lean/lake/Lake/Config/Monad.lean %%DATADIR%%/src/lean/lake/Lake/Config/Opaque.lean +%%DATADIR%%/src/lean/lake/Lake/Config/OutFormat.lean %%DATADIR%%/src/lean/lake/Lake/Config/Package.lean +%%DATADIR%%/src/lean/lake/Lake/Config/Pattern.lean %%DATADIR%%/src/lean/lake/Lake/Config/Script.lean %%DATADIR%%/src/lean/lake/Lake/Config/TargetConfig.lean %%DATADIR%%/src/lean/lake/Lake/Config/Workspace.lean @@ -3345,11 +5107,14 @@ share/lean/lean.mk %%DATADIR%%/src/lean/lake/Lake/DSL/Config.lean %%DATADIR%%/src/lean/lake/Lake/DSL/DeclUtil.lean %%DATADIR%%/src/lean/lake/Lake/DSL/Extensions.lean +%%DATADIR%%/src/lean/lake/Lake/DSL/Key.lean %%DATADIR%%/src/lean/lake/Lake/DSL/Meta.lean %%DATADIR%%/src/lean/lake/Lake/DSL/Package.lean %%DATADIR%%/src/lean/lake/Lake/DSL/Require.lean %%DATADIR%%/src/lean/lake/Lake/DSL/Script.lean +%%DATADIR%%/src/lean/lake/Lake/DSL/Syntax.lean %%DATADIR%%/src/lean/lake/Lake/DSL/Targets.lean +%%DATADIR%%/src/lean/lake/Lake/DSL/VerLit.lean %%DATADIR%%/src/lean/lake/Lake/Load.lean %%DATADIR%%/src/lean/lake/Lake/Load/Config.lean %%DATADIR%%/src/lean/lake/Lake/Load/Lean.lean @@ -3361,7 +5126,6 @@ share/lean/lean.mk %%DATADIR%%/src/lean/lake/Lake/Load/Resolve.lean %%DATADIR%%/src/lean/lake/Lake/Load/Toml.lean %%DATADIR%%/src/lean/lake/Lake/Load/Workspace.lean -%%DATADIR%%/src/lean/lake/Lake/Main.lean %%DATADIR%%/src/lean/lake/Lake/Reservoir.lean %%DATADIR%%/src/lean/lake/Lake/Toml.lean %%DATADIR%%/src/lean/lake/Lake/Toml/Data.lean @@ -3382,6 +5146,7 @@ share/lean/lean.mk %%DATADIR%%/src/lean/lake/Lake/Util/Compare.lean %%DATADIR%%/src/lean/lake/Lake/Util/Cycle.lean %%DATADIR%%/src/lean/lake/Lake/Util/DRBMap.lean +%%DATADIR%%/src/lean/lake/Lake/Util/Date.lean %%DATADIR%%/src/lean/lake/Lake/Util/EStateT.lean %%DATADIR%%/src/lean/lake/Lake/Util/EquipT.lean %%DATADIR%%/src/lean/lake/Lake/Util/Error.lean @@ -3400,6 +5165,7 @@ share/lean/lean.mk %%DATADIR%%/src/lean/lake/Lake/Util/Name.lean %%DATADIR%%/src/lean/lake/Lake/Util/NativeLib.lean %%DATADIR%%/src/lean/lake/Lake/Util/Opaque.lean +%%DATADIR%%/src/lean/lake/Lake/Util/OpaqueType.lean %%DATADIR%%/src/lean/lake/Lake/Util/OrdHashSet.lean %%DATADIR%%/src/lean/lake/Lake/Util/OrderedTagAttribute.lean %%DATADIR%%/src/lean/lake/Lake/Util/Proc.lean @@ -3410,7 +5176,9 @@ share/lean/lean.mk %%DATADIR%%/src/lean/lake/Lake/Util/Task.lean %%DATADIR%%/src/lean/lake/Lake/Util/Version.lean %%DATADIR%%/src/lean/lake/Lake/Version.lean +%%DATADIR%%/src/lean/lake/LakeMain.lean %%DATADIR%%/src/lean/lake/README.md +%%DATADIR%%/src/lean/lake/tests/api/keys.lean %%DATADIR%%/src/lean/lake/tests/badImport/Etc.lean %%DATADIR%%/src/lean/lake/tests/badImport/Lib/B.lean %%DATADIR%%/src/lean/lake/tests/badImport/Lib/B1.lean @@ -3439,12 +5207,21 @@ share/lean/lean.mk %%DATADIR%%/src/lean/lake/tests/driver/script.lean %%DATADIR%%/src/lean/lake/tests/driver/two.lean %%DATADIR%%/src/lean/lake/tests/driver/unknown.lean +%%DATADIR%%/src/lean/lake/tests/externLib/Main.lean +%%DATADIR%%/src/lean/lake/tests/externLib/Test.lean +%%DATADIR%%/src/lean/lake/tests/externLib/ffi/FFI.lean +%%DATADIR%%/src/lean/lake/tests/externLib/ffi/Main.lean +%%DATADIR%%/src/lean/lake/tests/externLib/ffi/lakefile.lean %%DATADIR%%/src/lean/lake/tests/globs/TBA.lean %%DATADIR%%/src/lean/lake/tests/globs/TBA/Eulerian.lean %%DATADIR%%/src/lean/lake/tests/globs/TBA/Eulerian/A.lean %%DATADIR%%/src/lean/lake/tests/globs/Test/1.lean %%DATADIR%%/src/lean/lake/tests/globs/Test/Subtest/1.lean %%DATADIR%%/src/lean/lake/tests/globs/lakefile.lean +%%DATADIR%%/src/lean/lake/tests/inputFile/lakefile.expected.lean +%%DATADIR%%/src/lean/lake/tests/inputFile/lakefileAlt.lean +%%DATADIR%%/src/lean/lake/tests/inputFile/test.lean +%%DATADIR%%/src/lean/lake/tests/kinds/lakefile.lean %%DATADIR%%/src/lean/lake/tests/lean/Lib.lean %%DATADIR%%/src/lean/lake/tests/lean/Lib/Basic.lean %%DATADIR%%/src/lean/lake/tests/lean/Test.lean @@ -3469,9 +5246,11 @@ share/lean/lean.mk %%DATADIR%%/src/lean/lake/tests/noBuild/Test.lean %%DATADIR%%/src/lean/lake/tests/noBuild/lakefile.lean %%DATADIR%%/src/lean/lake/tests/noRelease/Test.lean +%%DATADIR%%/src/lean/lake/tests/noRelease/dep/Dep.lean %%DATADIR%%/src/lean/lake/tests/noRelease/dep/lakefile.lean %%DATADIR%%/src/lean/lake/tests/noRelease/lakefile.lean -%%DATADIR%%/src/lean/lake/tests/online/lakefile.lean +%%DATADIR%%/src/lean/lake/tests/online/barrel.lean +%%DATADIR%%/src/lean/lake/tests/online/require.lean %%DATADIR%%/src/lean/lake/tests/order/A.lean %%DATADIR%%/src/lean/lake/tests/order/A/B.lean %%DATADIR%%/src/lean/lake/tests/order/A/B/C.lean @@ -3479,27 +5258,49 @@ share/lean/lean.mk %%DATADIR%%/src/lean/lake/tests/order/bar/X.lean %%DATADIR%%/src/lean/lake/tests/order/bar/Y.lean %%DATADIR%%/src/lean/lake/tests/order/bar/lakefile.lean +%%DATADIR%%/src/lean/lake/tests/order/baz/X.lean +%%DATADIR%%/src/lean/lake/tests/order/baz/lakefile.lean %%DATADIR%%/src/lean/lake/tests/order/foo/X.lean %%DATADIR%%/src/lean/lake/tests/order/foo/Y.lean %%DATADIR%%/src/lean/lake/tests/order/foo/lakefile.lean %%DATADIR%%/src/lean/lake/tests/order/lakefile.lean %%DATADIR%%/src/lean/lake/tests/order/leaf/Z.lean %%DATADIR%%/src/lean/lake/tests/order/leaf/lakefile.lean +%%DATADIR%%/src/lean/lake/tests/packageOverrides/bar1/bar.lean +%%DATADIR%%/src/lean/lake/tests/packageOverrides/bar2/bar.lean +%%DATADIR%%/src/lean/lake/tests/packageOverrides/foo/foo.lean +%%DATADIR%%/src/lean/lake/tests/packageOverrides/lakefile.lean %%DATADIR%%/src/lean/lake/tests/postUpdate/dep/hello.lean %%DATADIR%%/src/lean/lake/tests/postUpdate/dep/lakefile.lean %%DATADIR%%/src/lean/lake/tests/postUpdate/lakefile.lean -%%DATADIR%%/src/lean/lake/tests/precompileArgs/Foo.lean -%%DATADIR%%/src/lean/lake/tests/precompileArgs/Foo/Bar.lean -%%DATADIR%%/src/lean/lake/tests/precompileArgs/lakefile.lean +%%DATADIR%%/src/lean/lake/tests/precompileLink/Downstream.lean +%%DATADIR%%/src/lean/lake/tests/precompileLink/Downstream/Import.lean +%%DATADIR%%/src/lean/lake/tests/precompileLink/Foo.lean +%%DATADIR%%/src/lean/lake/tests/precompileLink/Foo/Bar.lean +%%DATADIR%%/src/lean/lake/tests/precompileLink/Foo/Baz.lean +%%DATADIR%%/src/lean/lake/tests/precompileLink/FooDep.lean +%%DATADIR%%/src/lean/lake/tests/precompileLink/FooDepDep.lean +%%DATADIR%%/src/lean/lake/tests/precompileLink/Indirect.lean +%%DATADIR%%/src/lean/lake/tests/precompileLink/lakefile.lean +%%DATADIR%%/src/lean/lake/tests/precompileLink/orderTest.lean +%%DATADIR%%/src/lean/lake/tests/query/exe.lean +%%DATADIR%%/src/lean/lake/tests/query/lakefile.lean +%%DATADIR%%/src/lean/lake/tests/query/lib/A.lean +%%DATADIR%%/src/lean/lake/tests/query/lib/B.lean +%%DATADIR%%/src/lean/lake/tests/query/lib/C.lean %%DATADIR%%/src/lean/lake/tests/rebuild/Main.lean %%DATADIR%%/src/lean/lake/tests/rebuild/lakefile.lean %%DATADIR%%/src/lean/lake/tests/reservoirConfig/lakefile.lean %%DATADIR%%/src/lean/lake/tests/reversion/Hello.lean %%DATADIR%%/src/lean/lake/tests/reversion/Main.lean %%DATADIR%%/src/lean/lake/tests/reversion/lakefile.lean +%%DATADIR%%/src/lean/lake/tests/setupFile/Test.lean +%%DATADIR%%/src/lean/lake/tests/setupFile/invalid.lean %%DATADIR%%/src/lean/lake/tests/toml/README.md %%DATADIR%%/src/lean/lake/tests/toml/Test.lean +%%DATADIR%%/src/lean/lake/tests/toolchain/lakefile.lean %%DATADIR%%/src/lean/lake/tests/trace/Foo.lean %%DATADIR%%/src/lean/lake/tests/translateConfig/out.expected.lean %%DATADIR%%/src/lean/lake/tests/translateConfig/source.lean +%%DATADIR%%/src/lean/lake/tests/updateToolchain/test.lean %%DATADIR%%/src/lean/lake/tests/versionTags/lakefile.lean |