summaryrefslogtreecommitdiff
path: root/math
diff options
context:
space:
mode:
Diffstat (limited to 'math')
-rw-r--r--math/R-cran-terra/Makefile2
-rw-r--r--math/R-cran-terra/distinfo6
-rw-r--r--math/e-antic/Makefile5
-rw-r--r--math/e-antic/distinfo6
-rw-r--r--math/e-antic/pkg-plist4
-rw-r--r--math/lean4/Makefile13
-rw-r--r--math/lean4/distinfo6
-rw-r--r--math/lean4/files/patch-src_CMakeLists.txt13
-rw-r--r--math/lean4/files/patch-src_bin_leanc.in11
-rw-r--r--math/lean4/files/patch-src_runtime_io.cpp4
-rw-r--r--math/lean4/files/patch-src_runtime_process.cpp22
-rw-r--r--math/lean4/files/patch-src_runtime_stack__overflow.cpp6
-rw-r--r--math/lean4/files/patch-stage0_src_CMakeLists.txt13
-rw-r--r--math/lean4/files/patch-stage0_src_bin_leanc.in11
-rw-r--r--math/lean4/files/patch-stage0_src_runtime_io.cpp4
-rw-r--r--math/lean4/files/patch-stage0_src_runtime_process.cpp22
-rw-r--r--math/lean4/files/patch-stage0_src_runtime_stack__overflow.cpp6
-rw-r--r--math/lean4/pkg-plist2025
-rw-r--r--math/manifold/Makefile7
19 files changed, 2034 insertions, 152 deletions
diff --git a/math/R-cran-terra/Makefile b/math/R-cran-terra/Makefile
index 927ac25dac86..61bebcb8274b 100644
--- a/math/R-cran-terra/Makefile
+++ b/math/R-cran-terra/Makefile
@@ -1,5 +1,5 @@
PORTNAME= terra
-DISTVERSION= 1.8-42
+DISTVERSION= 1.8-50
CATEGORIES= math
DISTNAME= ${PORTNAME}_${DISTVERSION}
diff --git a/math/R-cran-terra/distinfo b/math/R-cran-terra/distinfo
index 4cf87c62ddc3..84d902e2d47f 100644
--- a/math/R-cran-terra/distinfo
+++ b/math/R-cran-terra/distinfo
@@ -1,3 +1,3 @@
-TIMESTAMP = 1743845360
-SHA256 (terra_1.8-42.tar.gz) = d4590ce7cbc9421cc4008a487a0f66f7c326b6420978d5361b9481fba4d4342e
-SIZE (terra_1.8-42.tar.gz) = 1030778
+TIMESTAMP = 1746911385
+SHA256 (terra_1.8-50.tar.gz) = 5e207c138da9623b536e5f478811196a5930cb132f894df0cd249e62c54654ef
+SIZE (terra_1.8-50.tar.gz) = 1034549
diff --git a/math/e-antic/Makefile b/math/e-antic/Makefile
index d04d7bb22da5..7cd6bd10f363 100644
--- a/math/e-antic/Makefile
+++ b/math/e-antic/Makefile
@@ -1,12 +1,11 @@
PORTNAME= e-antic
-DISTVERSION= 2.0.2
-PORTREVISION= 6
+DISTVERSION= 2.1.0
#MASTER_SITES= https://www.labri.fr/perso/vdelecro/e-antic/
CATEGORIES= math
MAINTAINER= thierry@FreeBSD.org
COMMENT= Real Embedded Algebraic Number Theory In C
-WWW= https://github.com/flatsurf/e-antic
+WWW= https://flatsurf.github.io/e-antic/
LICENSE= GPLv3 LGPL3
LICENSE_COMB= dual
diff --git a/math/e-antic/distinfo b/math/e-antic/distinfo
index 147e7eb9cfbf..7cfde042f1aa 100644
--- a/math/e-antic/distinfo
+++ b/math/e-antic/distinfo
@@ -1,6 +1,6 @@
-TIMESTAMP = 1714844465
-SHA256 (flatsurf-e-antic-2.0.2_GH0.tar.gz) = 679b21f20af76d8992f8006b4701785acda33564f4bfae4732621b9e2ed23dcb
-SIZE (flatsurf-e-antic-2.0.2_GH0.tar.gz) = 162098
+TIMESTAMP = 1746722529
+SHA256 (flatsurf-e-antic-2.1.0_GH0.tar.gz) = 183a7b9f33ec0bda428d8ac463700a7386502babac83cef83398fcaed2cda6d2
+SIZE (flatsurf-e-antic-2.1.0_GH0.tar.gz) = 378850
SHA256 (catchorg-Catch2-62fd660_GH0.tar.gz) = 6ffb927225dcae98bcb3f1af908f2cc5cd9a71cfdb29f7a3995aad1fd8336840
SIZE (catchorg-Catch2-62fd660_GH0.tar.gz) = 661905
SHA256 (USCiLab-cereal-ebef1e9_GH0.tar.gz) = 14567f3df18057b820a99ce027fe1a830fdf8b42720efa982af9b86fef67f262
diff --git a/math/e-antic/pkg-plist b/math/e-antic/pkg-plist
index 123fc2039e56..03f301828e9c 100644
--- a/math/e-antic/pkg-plist
+++ b/math/e-antic/pkg-plist
@@ -16,11 +16,11 @@ include/libeantic/local.h
lib/libeantic.a
lib/libeantic.so
lib/libeantic.so.3
-lib/libeantic.so.3.0.2
+lib/libeantic.so.3.1.0
lib/libeanticxx.a
lib/libeanticxx.so
lib/libeanticxx.so.3
-lib/libeanticxx.so.3.0.2
+lib/libeanticxx.so.3.1.0
%%PYTHON_SITELIBDIR%%/pyeantic-%%VER%%-py%%PYTHON_VER%%.egg-info/PKG-INFO
%%PYTHON_SITELIBDIR%%/pyeantic-%%VER%%-py%%PYTHON_VER%%.egg-info/SOURCES.txt
%%PYTHON_SITELIBDIR%%/pyeantic-%%VER%%-py%%PYTHON_VER%%.egg-info/dependency_links.txt
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
diff --git a/math/manifold/Makefile b/math/manifold/Makefile
index b0a58d18e12e..f15d9c8f5851 100644
--- a/math/manifold/Makefile
+++ b/math/manifold/Makefile
@@ -34,6 +34,13 @@ CMAKE_OFF= MANIFOLD_DOWNLOADS \
USE_LDCONFIG= yes
+.include <bsd.port.options.mk>
+
+pre-configure:
+.if ${ARCH} == "i386" || ${ARCH} == "armv7"
+ ${REINPLACE_CMD} -e 's|-Werror|-Wno-format|' ${WRKSRC}/CMakeLists.txt
+.endif
+
do-test:
(cd ${BUILD_WRKSRC}/test && ./manifold_test)