Date: Fri, 27 Feb 2026 07:22:43 +0000 From: Yuri Victorovich <yuri@FreeBSD.org> To: ports-committers@FreeBSD.org, dev-commits-ports-all@FreeBSD.org, dev-commits-ports-main@FreeBSD.org Subject: git: 4cf61e688850 - main - math/lean4: update 4.25.2-2025=?utf-8?Q?1201 =E2=86=92?= 4.29.0.r2 Message-ID: <69a14643.469ac.51d3da42@gitrepo.freebsd.org>
index | next in thread | raw e-mail
The branch main has been updated by yuri: URL: https://cgit.FreeBSD.org/ports/commit/?id=4cf61e68885083d205936ea3c35eb89abd3fa3ee commit 4cf61e68885083d205936ea3c35eb89abd3fa3ee Author: Yuri Victorovich <yuri@FreeBSD.org> AuthorDate: 2026-02-27 05:55:57 +0000 Commit: Yuri Victorovich <yuri@FreeBSD.org> CommitDate: 2026-02-27 07:22:39 +0000 math/lean4: update 4.25.2-20251201 → 4.29.0.r2 --- math/lean4/Makefile | 4 +- math/lean4/distinfo | 6 +- math/lean4/files/patch-src_CMakeLists.txt | 43 +- math/lean4/files/patch-src_runtime_io.cpp | 4 +- math/lean4/files/patch-src_runtime_process.cpp | 4 +- math/lean4/files/patch-src_runtime_thread.h | 25 + math/lean4/files/patch-stage0_src_CMakeLists.txt | 43 +- math/lean4/files/patch-stage0_src_runtime_io.cpp | 4 +- .../files/patch-stage0_src_runtime_process.cpp | 4 +- math/lean4/files/patch-stage0_src_runtime_thread.h | 25 + math/lean4/files/patch-tests_lakefile.toml | 10 +- math/lean4/pkg-plist | 1323 +++++++++++++++++--- 12 files changed, 1252 insertions(+), 243 deletions(-) diff --git a/math/lean4/Makefile b/math/lean4/Makefile index 8b5c81aa12bc..0ee800616f73 100644 --- a/math/lean4/Makefile +++ b/math/lean4/Makefile @@ -1,6 +1,6 @@ PORTNAME= lean4 DISTVERSIONPREFIX= v -DISTVERSION= 4.25.2-20251201 +DISTVERSION= 4.29.0-rc2 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 @@ -25,7 +25,6 @@ USES= cmake:noninja,testing compiler:c++14-lang gmake pkgconfig python:build # USE_GITHUB= yes GH_ACCOUNT= leanprover -GH_TAGNAME= 5e165e3 CFLAGS+= -fPIC CXXFLAGS+= -fPIC @@ -79,5 +78,6 @@ post-install: lib/lean/libLake_shared.so # tests as of 4.25.2-20251201: 100% tests passed, 0 tests failed out of 3367 +# tests as of 4.29.0-rc2: 99% tests passed, 12 tests failed out of 3584, see https://github.com/leanprover/lean4/issues/12721 .include <bsd.port.mk> diff --git a/math/lean4/distinfo b/math/lean4/distinfo index 20923ac21be3..ea48da926973 100644 --- a/math/lean4/distinfo +++ b/math/lean4/distinfo @@ -1,3 +1,3 @@ -TIMESTAMP = 1764606890 -SHA256 (leanprover-lean4-v4.25.2-20251201-5e165e3_GH0.tar.gz) = 70c7265936d4d5393c9778a19d39620b4ce51c75cda1a0d3fbdef685996c5d3d -SIZE (leanprover-lean4-v4.25.2-20251201-5e165e3_GH0.tar.gz) = 48235866 +TIMESTAMP = 1772136453 +SHA256 (leanprover-lean4-v4.29.0-rc2_GH0.tar.gz) = 72dc439deaf313ffb032355fd2589f94a04ed19ee5e3d05d49091f02b94ae779 +SIZE (leanprover-lean4-v4.29.0-rc2_GH0.tar.gz) = 52612906 diff --git a/math/lean4/files/patch-src_CMakeLists.txt b/math/lean4/files/patch-src_CMakeLists.txt index d71c117b8802..c7e42796fdc2 100644 --- a/math/lean4/files/patch-src_CMakeLists.txt +++ b/math/lean4/files/patch-src_CMakeLists.txt @@ -1,8 +1,17 @@ ---- src/CMakeLists.txt.orig 2025-11-18 02:29:21 UTC +--- src/CMakeLists.txt.orig 2026-02-24 00:20:30 UTC +++ src/CMakeLists.txt -@@ -473,6 +473,17 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Linux") - string(APPEND TOOLCHAIN_SHARED_LINKER_FLAGS " -Wl,-rpath=\\$$ORIGIN/..:\\$$ORIGIN") - string(APPEND LAKESHARED_LINKER_FLAGS " -Wl,--whole-archive ${CMAKE_BINARY_DIR}/lib/lean/libLake.a.export -Wl,--no-whole-archive") +@@ -517,7 +517,7 @@ endif() + string(APPEND LEAN_EXTRA_LINKER_FLAGS " -lm") + endif() + +-if(CMAKE_SYSTEM_NAME MATCHES "Linux") ++if(CMAKE_SYSTEM_NAME MATCHES "Linux|FreeBSD") + if(BSYMBOLIC) + string(APPEND LEANC_SHARED_LINKER_FLAGS " -Wl,-Bsymbolic") + string(APPEND TOOLCHAIN_SHARED_LINKER_FLAGS " -Wl,-Bsymbolic") +@@ -530,6 +530,19 @@ if(CMAKE_SYSTEM_NAME MATCHES "Linux") + " -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) @@ -12,13 +21,15 @@ + 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 LAKESHARED_LINKER_FLAGS " -Wl,--whole-archive ${CMAKE_BINARY_DIR}/lib/lean/libLake.a.export -Wl,--no-whole-archive") ++ 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") -+ set(LEAN_EXTRA_LAKEFILE_TOML "weakLeancArgs = [\"-fPIC\"]") - elseif(${CMAKE_SYSTEM_NAME} MATCHES "Darwin") + 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") -@@ -586,6 +597,9 @@ string(APPEND LEANC_OPTS " -I${CMAKE_BINARY_DIR}/inclu +@@ -653,6 +666,9 @@ string(APPEND LEANC_OPTS " -I${CMAKE_BINARY_DIR}/inclu # Lean code only needs this one include string(APPEND LEANC_OPTS " -I${CMAKE_BINARY_DIR}/include") @@ -28,12 +39,12 @@ # Use CMake profile C++ flags for building Lean libraries, but do not embed in `leanc` string(TOUPPER "${CMAKE_BUILD_TYPE}" uppercase_CMAKE_BUILD_TYPE) string(APPEND LEANC_OPTS " ${CMAKE_CXX_FLAGS_${uppercase_CMAKE_BUILD_TYPE}}") -@@ -814,7 +828,7 @@ endif() - file(CREATE_LINK ${CMAKE_SOURCE_DIR} ${CMAKE_BINARY_DIR}/src/lean RESULT _IGNORE_RES SYMBOLIC) - endif() +@@ -939,7 +955,7 @@ install( --install(DIRECTORY "${CMAKE_SOURCE_DIR}/" DESTINATION src/lean -+install(DIRECTORY "${CMAKE_SOURCE_DIR}/" DESTINATION share/lean4/src/lean - FILES_MATCHING - PATTERN "*.lean" - PATTERN "*.md" + install( + DIRECTORY "${CMAKE_SOURCE_DIR}/" +- DESTINATION src/lean ++ DESTINATION share/lean4/src/lean + FILES_MATCHING + PATTERN "*.lean" + PATTERN "*.md" diff --git a/math/lean4/files/patch-src_runtime_io.cpp b/math/lean4/files/patch-src_runtime_io.cpp index 8fe17f4e138b..5f5125a68dc9 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 2025-11-18 02:29:21 UTC +--- src/runtime/io.cpp.orig 2026-02-24 00:20:30 UTC +++ src/runtime/io.cpp -@@ -1365,7 +1365,13 @@ extern "C" LEAN_EXPORT obj_res lean_io_app_path(obj_ar +@@ -1390,7 +1390,13 @@ extern "C" LEAN_EXPORT obj_res lean_io_app_path() { 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 index b13998f4743f..77ccdca7e634 100644 --- a/math/lean4/files/patch-src_runtime_process.cpp +++ b/math/lean4/files/patch-src_runtime_process.cpp @@ -1,4 +1,4 @@ ---- src/runtime/process.cpp.orig 2025-05-06 09:12:17 UTC +--- src/runtime/process.cpp.orig 2026-02-24 00:20:30 UTC +++ src/runtime/process.cpp @@ -31,6 +31,10 @@ Author: Jared Roesch #include <sys/syscall.h> @@ -11,7 +11,7 @@ #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 +@@ -343,6 +347,8 @@ extern "C" LEAN_EXPORT uint64_t lean_io_get_tid() { lean_always_assert(pthread_threadid_np(NULL, &tid) == 0); #elif defined(LEAN_EMSCRIPTEN) tid = 0; diff --git a/math/lean4/files/patch-src_runtime_thread.h b/math/lean4/files/patch-src_runtime_thread.h new file mode 100644 index 000000000000..ad92908b8823 --- /dev/null +++ b/math/lean4/files/patch-src_runtime_thread.h @@ -0,0 +1,25 @@ +--- src/runtime/thread.h.orig 2026-01-20 14:00:20 UTC ++++ src/runtime/thread.h +@@ -179,11 +179,20 @@ template<typename T> class unique_lock { + ~lock_guard() {} + }; + template<typename T> class unique_lock { ++private: ++ bool m_owns_lock; + public: +- unique_lock(T const &) {} +- ~unique_lock() {} ++ unique_lock(T const &) : m_owns_lock(true) {} ++ template<typename Mutex> ++ unique_lock(Mutex const &, std::adopt_lock_t) : m_owns_lock(true) {} ++ ~unique_lock() { ++ if (m_owns_lock) unlock(); ++ } + void lock() {} + void unlock() {} ++ void release() { ++ m_owns_lock = false; ++ } + }; + inline unsigned hardware_concurrency() { return 1; } + } diff --git a/math/lean4/files/patch-stage0_src_CMakeLists.txt b/math/lean4/files/patch-stage0_src_CMakeLists.txt index 7ec7241aa2f2..b3e4a48d592e 100644 --- a/math/lean4/files/patch-stage0_src_CMakeLists.txt +++ b/math/lean4/files/patch-stage0_src_CMakeLists.txt @@ -1,8 +1,17 @@ ---- stage0/src/CMakeLists.txt.orig 2025-11-18 02:29:21 UTC +--- stage0/src/CMakeLists.txt.orig 2026-02-24 00:20:30 UTC +++ stage0/src/CMakeLists.txt -@@ -473,6 +473,17 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Linux") - string(APPEND TOOLCHAIN_SHARED_LINKER_FLAGS " -Wl,-rpath=\\$$ORIGIN/..:\\$$ORIGIN") - string(APPEND LAKESHARED_LINKER_FLAGS " -Wl,--whole-archive ${CMAKE_BINARY_DIR}/lib/lean/libLake.a.export -Wl,--no-whole-archive") +@@ -517,7 +517,7 @@ endif() + string(APPEND LEAN_EXTRA_LINKER_FLAGS " -lm") + endif() + +-if(CMAKE_SYSTEM_NAME MATCHES "Linux") ++if(CMAKE_SYSTEM_NAME MATCHES "Linux|FreeBSD") + if(BSYMBOLIC) + string(APPEND LEANC_SHARED_LINKER_FLAGS " -Wl,-Bsymbolic") + string(APPEND TOOLCHAIN_SHARED_LINKER_FLAGS " -Wl,-Bsymbolic") +@@ -530,6 +530,19 @@ if(CMAKE_SYSTEM_NAME MATCHES "Linux") + " -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) @@ -12,13 +21,15 @@ + 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 LAKESHARED_LINKER_FLAGS " -Wl,--whole-archive ${CMAKE_BINARY_DIR}/lib/lean/libLake.a.export -Wl,--no-whole-archive") ++ 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") -+ set(LEAN_EXTRA_LAKEFILE_TOML "weakLeancArgs = [\"-fPIC\"]") - elseif(${CMAKE_SYSTEM_NAME} MATCHES "Darwin") + 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") -@@ -586,6 +597,9 @@ string(APPEND LEANC_OPTS " -I${CMAKE_BINARY_DIR}/inclu +@@ -653,6 +666,9 @@ string(APPEND LEANC_OPTS " -I${CMAKE_BINARY_DIR}/inclu # Lean code only needs this one include string(APPEND LEANC_OPTS " -I${CMAKE_BINARY_DIR}/include") @@ -28,12 +39,12 @@ # Use CMake profile C++ flags for building Lean libraries, but do not embed in `leanc` string(TOUPPER "${CMAKE_BUILD_TYPE}" uppercase_CMAKE_BUILD_TYPE) string(APPEND LEANC_OPTS " ${CMAKE_CXX_FLAGS_${uppercase_CMAKE_BUILD_TYPE}}") -@@ -814,7 +828,7 @@ endif() - file(CREATE_LINK ${CMAKE_SOURCE_DIR} ${CMAKE_BINARY_DIR}/src/lean RESULT _IGNORE_RES SYMBOLIC) - endif() +@@ -939,7 +955,7 @@ install( --install(DIRECTORY "${CMAKE_SOURCE_DIR}/" DESTINATION src/lean -+install(DIRECTORY "${CMAKE_SOURCE_DIR}/" DESTINATION share/lean4/src/lean - FILES_MATCHING - PATTERN "*.lean" - PATTERN "*.md" + install( + DIRECTORY "${CMAKE_SOURCE_DIR}/" +- DESTINATION src/lean ++ DESTINATION share/lean4/src/lean + FILES_MATCHING + PATTERN "*.lean" + PATTERN "*.md" diff --git a/math/lean4/files/patch-stage0_src_runtime_io.cpp b/math/lean4/files/patch-stage0_src_runtime_io.cpp index 9b00b760a7a8..ed9e0e2c8895 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 2025-05-06 09:12:17 UTC +--- stage0/src/runtime/io.cpp.orig 2026-02-24 00:20:30 UTC +++ stage0/src/runtime/io.cpp -@@ -1253,7 +1253,13 @@ extern "C" LEAN_EXPORT obj_res lean_io_app_path(obj_ar +@@ -1390,7 +1390,13 @@ extern "C" LEAN_EXPORT obj_res lean_io_app_path() { 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 index 8b8fb1a9e008..8afb98973c6b 100644 --- a/math/lean4/files/patch-stage0_src_runtime_process.cpp +++ b/math/lean4/files/patch-stage0_src_runtime_process.cpp @@ -1,4 +1,4 @@ ---- stage0/src/runtime/process.cpp.orig 2025-05-06 09:12:17 UTC +--- stage0/src/runtime/process.cpp.orig 2026-02-24 00:20:30 UTC +++ stage0/src/runtime/process.cpp @@ -31,6 +31,10 @@ Author: Jared Roesch #include <sys/syscall.h> @@ -11,7 +11,7 @@ #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 +@@ -343,6 +347,8 @@ extern "C" LEAN_EXPORT uint64_t lean_io_get_tid() { lean_always_assert(pthread_threadid_np(NULL, &tid) == 0); #elif defined(LEAN_EMSCRIPTEN) tid = 0; diff --git a/math/lean4/files/patch-stage0_src_runtime_thread.h b/math/lean4/files/patch-stage0_src_runtime_thread.h new file mode 100644 index 000000000000..df98ed48ece9 --- /dev/null +++ b/math/lean4/files/patch-stage0_src_runtime_thread.h @@ -0,0 +1,25 @@ +--- stage0/src/runtime/thread.h.orig 2026-01-20 14:00:20 UTC ++++ stage0/src/runtime/thread.h +@@ -179,11 +179,20 @@ template<typename T> class unique_lock { + ~lock_guard() {} + }; + template<typename T> class unique_lock { ++private: ++ bool m_owns_lock; + public: +- unique_lock(T const &) {} +- ~unique_lock() {} ++ unique_lock(T const &) : m_owns_lock(true) {} ++ template<typename Mutex> ++ unique_lock(Mutex const &, std::adopt_lock_t) : m_owns_lock(true) {} ++ ~unique_lock() { ++ if (m_owns_lock) unlock(); ++ } + void lock() {} + void unlock() {} ++ void release() { ++ m_owns_lock = false; ++ } + }; + inline unsigned hardware_concurrency() { return 1; } + } diff --git a/math/lean4/files/patch-tests_lakefile.toml b/math/lean4/files/patch-tests_lakefile.toml index 3a01b013943d..362bb9408419 100644 --- a/math/lean4/files/patch-tests_lakefile.toml +++ b/math/lean4/files/patch-tests_lakefile.toml @@ -1,10 +1,10 @@ ---- tests/lakefile.toml.orig 2025-11-17 18:29:21 UTC +--- tests/lakefile.toml.orig 2026-01-20 14:00:20 UTC +++ tests/lakefile.toml -@@ -1,5 +1,7 @@ +@@ -1,5 +1,7 @@ name = "tests" name = "tests" +weakLeancArgs = ["-fPIC"] + - # Allow `module` in tests when opened in the language server. - # Enabled during actual test runs in the respective test_single.sh. - moreGlobalServerArgs = ["-Dexperimental.module=true"] + [[lean_lib]] + name = "Tests" + globs = ["lean.*"] diff --git a/math/lean4/pkg-plist b/math/lean4/pkg-plist index ae09be366a40..69bb2506dd50 100644 --- a/math/lean4/pkg-plist +++ b/math/lean4/pkg-plist @@ -1,6 +1,7 @@ bin/lake bin/lean bin/leanc +bin/leanchecker bin/leanmake include/lean/config.h include/lean/lean.h @@ -47,6 +48,11 @@ lib/lean/Init/Control/Basic.ir lib/lean/Init/Control/Basic.olean lib/lean/Init/Control/Basic.olean.private lib/lean/Init/Control/Basic.olean.server +lib/lean/Init/Control/Do.ilean +lib/lean/Init/Control/Do.ir +lib/lean/Init/Control/Do.olean +lib/lean/Init/Control/Do.olean.private +lib/lean/Init/Control/Do.olean.server lib/lean/Init/Control/EState.ilean lib/lean/Init/Control/EState.ir lib/lean/Init/Control/EState.olean @@ -87,6 +93,21 @@ lib/lean/Init/Control/Lawful/Lemmas.ir 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/Lawful/MonadAttach.ilean +lib/lean/Init/Control/Lawful/MonadAttach.ir +lib/lean/Init/Control/Lawful/MonadAttach.olean +lib/lean/Init/Control/Lawful/MonadAttach.olean.private +lib/lean/Init/Control/Lawful/MonadAttach.olean.server +lib/lean/Init/Control/Lawful/MonadAttach/Instances.ilean +lib/lean/Init/Control/Lawful/MonadAttach/Instances.ir +lib/lean/Init/Control/Lawful/MonadAttach/Instances.olean +lib/lean/Init/Control/Lawful/MonadAttach/Instances.olean.private +lib/lean/Init/Control/Lawful/MonadAttach/Instances.olean.server +lib/lean/Init/Control/Lawful/MonadAttach/Lemmas.ilean +lib/lean/Init/Control/Lawful/MonadAttach/Lemmas.ir +lib/lean/Init/Control/Lawful/MonadAttach/Lemmas.olean +lib/lean/Init/Control/Lawful/MonadAttach/Lemmas.olean.private +lib/lean/Init/Control/Lawful/MonadAttach/Lemmas.olean.server lib/lean/Init/Control/Lawful/MonadLift.ilean lib/lean/Init/Control/Lawful/MonadLift.ir lib/lean/Init/Control/Lawful/MonadLift.olean @@ -107,6 +128,11 @@ lib/lean/Init/Control/Lawful/MonadLift/Lemmas.ir lib/lean/Init/Control/Lawful/MonadLift/Lemmas.olean lib/lean/Init/Control/Lawful/MonadLift/Lemmas.olean.private lib/lean/Init/Control/Lawful/MonadLift/Lemmas.olean.server +lib/lean/Init/Control/MonadAttach.ilean +lib/lean/Init/Control/MonadAttach.ir +lib/lean/Init/Control/MonadAttach.olean +lib/lean/Init/Control/MonadAttach.olean.private +lib/lean/Init/Control/MonadAttach.olean.server lib/lean/Init/Control/Option.ilean lib/lean/Init/Control/Option.ir lib/lean/Init/Control/Option.olean @@ -227,6 +253,11 @@ lib/lean/Init/Data/Array/InsertionSort.ir 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/Int.ilean +lib/lean/Init/Data/Array/Int.ir +lib/lean/Init/Data/Array/Int.olean +lib/lean/Init/Data/Array/Int.olean.private +lib/lean/Init/Data/Array/Int.olean.server lib/lean/Init/Data/Array/Lemmas.ilean lib/lean/Init/Data/Array/Lemmas.ir lib/lean/Init/Data/Array/Lemmas.olean @@ -257,11 +288,21 @@ lib/lean/Init/Data/Array/Mem.ir 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/MinMax.ilean +lib/lean/Init/Data/Array/MinMax.ir +lib/lean/Init/Data/Array/MinMax.olean +lib/lean/Init/Data/Array/MinMax.olean.private +lib/lean/Init/Data/Array/MinMax.olean.server lib/lean/Init/Data/Array/Monadic.ilean lib/lean/Init/Data/Array/Monadic.ir 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/Nat.ilean +lib/lean/Init/Data/Array/Nat.ir +lib/lean/Init/Data/Array/Nat.olean +lib/lean/Init/Data/Array/Nat.olean.private +lib/lean/Init/Data/Array/Nat.olean.server lib/lean/Init/Data/Array/OfFn.ilean lib/lean/Init/Data/Array/OfFn.ir lib/lean/Init/Data/Array/OfFn.olean @@ -412,6 +453,11 @@ lib/lean/Init/Data/Char/Order.ir lib/lean/Init/Data/Char/Order.olean lib/lean/Init/Data/Char/Order.olean.private lib/lean/Init/Data/Char/Order.olean.server +lib/lean/Init/Data/Char/Ordinal.ilean +lib/lean/Init/Data/Char/Ordinal.ir +lib/lean/Init/Data/Char/Ordinal.olean +lib/lean/Init/Data/Char/Ordinal.olean.private +lib/lean/Init/Data/Char/Ordinal.olean.server lib/lean/Init/Data/Dyadic.ilean lib/lean/Init/Data/Dyadic.ir lib/lean/Init/Data/Dyadic.olean @@ -472,6 +518,11 @@ lib/lean/Init/Data/Fin/Log2.ir 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/Fin/OverflowAware.ilean +lib/lean/Init/Data/Fin/OverflowAware.ir +lib/lean/Init/Data/Fin/OverflowAware.olean +lib/lean/Init/Data/Fin/OverflowAware.olean.private +lib/lean/Init/Data/Fin/OverflowAware.olean.server lib/lean/Init/Data/Float.ilean lib/lean/Init/Data/Float.ir lib/lean/Init/Data/Float.olean @@ -737,6 +788,11 @@ lib/lean/Init/Data/Iterators/Consumers/Monadic/Partial.ir lib/lean/Init/Data/Iterators/Consumers/Monadic/Partial.olean lib/lean/Init/Data/Iterators/Consumers/Monadic/Partial.olean.private lib/lean/Init/Data/Iterators/Consumers/Monadic/Partial.olean.server +lib/lean/Init/Data/Iterators/Consumers/Monadic/Total.ilean +lib/lean/Init/Data/Iterators/Consumers/Monadic/Total.ir +lib/lean/Init/Data/Iterators/Consumers/Monadic/Total.olean +lib/lean/Init/Data/Iterators/Consumers/Monadic/Total.olean.private +lib/lean/Init/Data/Iterators/Consumers/Monadic/Total.olean.server lib/lean/Init/Data/Iterators/Consumers/Partial.ilean lib/lean/Init/Data/Iterators/Consumers/Partial.ir lib/lean/Init/Data/Iterators/Consumers/Partial.olean @@ -747,6 +803,11 @@ lib/lean/Init/Data/Iterators/Consumers/Stream.ir lib/lean/Init/Data/Iterators/Consumers/Stream.olean lib/lean/Init/Data/Iterators/Consumers/Stream.olean.private lib/lean/Init/Data/Iterators/Consumers/Stream.olean.server +lib/lean/Init/Data/Iterators/Consumers/Total.ilean +lib/lean/Init/Data/Iterators/Consumers/Total.ir +lib/lean/Init/Data/Iterators/Consumers/Total.olean +lib/lean/Init/Data/Iterators/Consumers/Total.olean.private +lib/lean/Init/Data/Iterators/Consumers/Total.olean.server lib/lean/Init/Data/Iterators/Internal.ilean lib/lean/Init/Data/Iterators/Internal.ir lib/lean/Init/Data/Iterators/Internal.olean @@ -757,11 +818,6 @@ lib/lean/Init/Data/Iterators/Internal/LawfulMonadLiftFunction.ir lib/lean/Init/Data/Iterators/Internal/LawfulMonadLiftFunction.olean lib/lean/Init/Data/Iterators/Internal/LawfulMonadLiftFunction.olean.private lib/lean/Init/Data/Iterators/Internal/LawfulMonadLiftFunction.olean.server -lib/lean/Init/Data/Iterators/Internal/Termination.ilean -lib/lean/Init/Data/Iterators/Internal/Termination.ir -lib/lean/Init/Data/Iterators/Internal/Termination.olean -lib/lean/Init/Data/Iterators/Internal/Termination.olean.private -lib/lean/Init/Data/Iterators/Internal/Termination.olean.server lib/lean/Init/Data/Iterators/Lemmas.ilean lib/lean/Init/Data/Iterators/Lemmas.ir lib/lean/Init/Data/Iterators/Lemmas.olean @@ -837,6 +893,11 @@ lib/lean/Init/Data/Iterators/Lemmas/Consumers.ir lib/lean/Init/Data/Iterators/Lemmas/Consumers.olean lib/lean/Init/Data/Iterators/Lemmas/Consumers.olean.private lib/lean/Init/Data/Iterators/Lemmas/Consumers.olean.server +lib/lean/Init/Data/Iterators/Lemmas/Consumers/Access.ilean +lib/lean/Init/Data/Iterators/Lemmas/Consumers/Access.ir +lib/lean/Init/Data/Iterators/Lemmas/Consumers/Access.olean +lib/lean/Init/Data/Iterators/Lemmas/Consumers/Access.olean.private +lib/lean/Init/Data/Iterators/Lemmas/Consumers/Access.olean.server lib/lean/Init/Data/Iterators/Lemmas/Consumers/Collect.ilean lib/lean/Init/Data/Iterators/Lemmas/Consumers/Collect.ir lib/lean/Init/Data/Iterators/Lemmas/Consumers/Collect.olean @@ -972,6 +1033,16 @@ lib/lean/Init/Data/List/Impl.ir 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/Int.ilean +lib/lean/Init/Data/List/Int.ir +lib/lean/Init/Data/List/Int.olean +lib/lean/Init/Data/List/Int.olean.private +lib/lean/Init/Data/List/Int.olean.server +lib/lean/Init/Data/List/Int/Sum.ilean +lib/lean/Init/Data/List/Int/Sum.ir +lib/lean/Init/Data/List/Int/Sum.olean +lib/lean/Init/Data/List/Int/Sum.olean.private +lib/lean/Init/Data/List/Int/Sum.olean.server lib/lean/Init/Data/List/Lemmas.ilean lib/lean/Init/Data/List/Lemmas.ir lib/lean/Init/Data/List/Lemmas.olean @@ -992,6 +1063,16 @@ lib/lean/Init/Data/List/MinMax.ir 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/MinMaxIdx.ilean +lib/lean/Init/Data/List/MinMaxIdx.ir +lib/lean/Init/Data/List/MinMaxIdx.olean +lib/lean/Init/Data/List/MinMaxIdx.olean.private +lib/lean/Init/Data/List/MinMaxIdx.olean.server +lib/lean/Init/Data/List/MinMaxOn.ilean +lib/lean/Init/Data/List/MinMaxOn.ir +lib/lean/Init/Data/List/MinMaxOn.olean +lib/lean/Init/Data/List/MinMaxOn.olean.private +lib/lean/Init/Data/List/MinMaxOn.olean.server lib/lean/Init/Data/List/Monadic.ilean lib/lean/Init/Data/List/Monadic.ir lib/lean/Init/Data/List/Monadic.olean @@ -1057,6 +1138,11 @@ lib/lean/Init/Data/List/Nat/Sublist.ir 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/Sum.ilean +lib/lean/Init/Data/List/Nat/Sum.ir +lib/lean/Init/Data/List/Nat/Sum.olean +lib/lean/Init/Data/List/Nat/Sum.olean.private +lib/lean/Init/Data/List/Nat/Sum.olean.server lib/lean/Init/Data/List/Nat/TakeDrop.ilean lib/lean/Init/Data/List/Nat/TakeDrop.ir lib/lean/Init/Data/List/Nat/TakeDrop.olean @@ -1087,6 +1173,21 @@ lib/lean/Init/Data/List/Range.ir 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/Scan.ilean +lib/lean/Init/Data/List/Scan.ir +lib/lean/Init/Data/List/Scan.olean +lib/lean/Init/Data/List/Scan.olean.private +lib/lean/Init/Data/List/Scan.olean.server +lib/lean/Init/Data/List/Scan/Basic.ilean +lib/lean/Init/Data/List/Scan/Basic.ir +lib/lean/Init/Data/List/Scan/Basic.olean +lib/lean/Init/Data/List/Scan/Basic.olean.private +lib/lean/Init/Data/List/Scan/Basic.olean.server +lib/lean/Init/Data/List/Scan/Lemmas.ilean +lib/lean/Init/Data/List/Scan/Lemmas.ir +lib/lean/Init/Data/List/Scan/Lemmas.olean +lib/lean/Init/Data/List/Scan/Lemmas.olean.private +lib/lean/Init/Data/List/Scan/Lemmas.olean.server lib/lean/Init/Data/List/Sort.ilean lib/lean/Init/Data/List/Sort.ir lib/lean/Init/Data/List/Sort.olean @@ -1242,6 +1343,16 @@ lib/lean/Init/Data/Nat/Power2.ir 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/Power2/Basic.ilean +lib/lean/Init/Data/Nat/Power2/Basic.ir +lib/lean/Init/Data/Nat/Power2/Basic.olean +lib/lean/Init/Data/Nat/Power2/Basic.olean.private +lib/lean/Init/Data/Nat/Power2/Basic.olean.server +lib/lean/Init/Data/Nat/Power2/Lemmas.ilean +lib/lean/Init/Data/Nat/Power2/Lemmas.ir +lib/lean/Init/Data/Nat/Power2/Lemmas.olean +lib/lean/Init/Data/Nat/Power2/Lemmas.olean.private +lib/lean/Init/Data/Nat/Power2/Lemmas.olean.server lib/lean/Init/Data/Nat/SOM.ilean lib/lean/Init/Data/Nat/SOM.ir lib/lean/Init/Data/Nat/SOM.olean @@ -1252,6 +1363,11 @@ lib/lean/Init/Data/Nat/Simproc.ir 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/Nat/ToString.ilean +lib/lean/Init/Data/Nat/ToString.ir +lib/lean/Init/Data/Nat/ToString.olean +lib/lean/Init/Data/Nat/ToString.olean.private +lib/lean/Init/Data/Nat/ToString.olean.server lib/lean/Init/Data/NeZero.ilean lib/lean/Init/Data/NeZero.ir lib/lean/Init/Data/NeZero.olean @@ -1292,6 +1408,11 @@ lib/lean/Init/Data/Option/Coe.ir 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/Function.ilean +lib/lean/Init/Data/Option/Function.ir +lib/lean/Init/Data/Option/Function.olean +lib/lean/Init/Data/Option/Function.olean.private +lib/lean/Init/Data/Option/Function.olean.server lib/lean/Init/Data/Option/Instances.ilean lib/lean/Init/Data/Option/Instances.ir lib/lean/Init/Data/Option/Instances.olean @@ -1387,6 +1508,16 @@ lib/lean/Init/Data/Order/LemmasExtra.ir lib/lean/Init/Data/Order/LemmasExtra.olean lib/lean/Init/Data/Order/LemmasExtra.olean.private lib/lean/Init/Data/Order/LemmasExtra.olean.server +lib/lean/Init/Data/Order/MinMaxOn.ilean +lib/lean/Init/Data/Order/MinMaxOn.ir +lib/lean/Init/Data/Order/MinMaxOn.olean +lib/lean/Init/Data/Order/MinMaxOn.olean.private +lib/lean/Init/Data/Order/MinMaxOn.olean.server +lib/lean/Init/Data/Order/Opposite.ilean +lib/lean/Init/Data/Order/Opposite.ir +lib/lean/Init/Data/Order/Opposite.olean +lib/lean/Init/Data/Order/Opposite.olean.private +lib/lean/Init/Data/Order/Opposite.olean.server lib/lean/Init/Data/Order/Ord.ilean lib/lean/Init/Data/Order/Ord.ir lib/lean/Init/Data/Order/Ord.olean @@ -1452,6 +1583,16 @@ lib/lean/Init/Data/Range/Polymorphic/BitVec.ir lib/lean/Init/Data/Range/Polymorphic/BitVec.olean lib/lean/Init/Data/Range/Polymorphic/BitVec.olean.private lib/lean/Init/Data/Range/Polymorphic/BitVec.olean.server +lib/lean/Init/Data/Range/Polymorphic/Char.ilean +lib/lean/Init/Data/Range/Polymorphic/Char.ir +lib/lean/Init/Data/Range/Polymorphic/Char.olean +lib/lean/Init/Data/Range/Polymorphic/Char.olean.private +lib/lean/Init/Data/Range/Polymorphic/Char.olean.server +lib/lean/Init/Data/Range/Polymorphic/Fin.ilean +lib/lean/Init/Data/Range/Polymorphic/Fin.ir +lib/lean/Init/Data/Range/Polymorphic/Fin.olean +lib/lean/Init/Data/Range/Polymorphic/Fin.olean.private +lib/lean/Init/Data/Range/Polymorphic/Fin.olean.server lib/lean/Init/Data/Range/Polymorphic/GetElemTactic.ilean lib/lean/Init/Data/Range/Polymorphic/GetElemTactic.ir lib/lean/Init/Data/Range/Polymorphic/GetElemTactic.olean @@ -1487,6 +1628,11 @@ lib/lean/Init/Data/Range/Polymorphic/Lemmas.ir lib/lean/Init/Data/Range/Polymorphic/Lemmas.olean lib/lean/Init/Data/Range/Polymorphic/Lemmas.olean.private lib/lean/Init/Data/Range/Polymorphic/Lemmas.olean.server +lib/lean/Init/Data/Range/Polymorphic/Map.ilean +lib/lean/Init/Data/Range/Polymorphic/Map.ir +lib/lean/Init/Data/Range/Polymorphic/Map.olean +lib/lean/Init/Data/Range/Polymorphic/Map.olean.private +lib/lean/Init/Data/Range/Polymorphic/Map.olean.server lib/lean/Init/Data/Range/Polymorphic/Nat.ilean lib/lean/Init/Data/Range/Polymorphic/Nat.ir lib/lean/Init/Data/Range/Polymorphic/Nat.olean @@ -1607,6 +1753,11 @@ lib/lean/Init/Data/Slice/Basic.ir lib/lean/Init/Data/Slice/Basic.olean lib/lean/Init/Data/Slice/Basic.olean.private lib/lean/Init/Data/Slice/Basic.olean.server +lib/lean/Init/Data/Slice/InternalLemmas.ilean +lib/lean/Init/Data/Slice/InternalLemmas.ir +lib/lean/Init/Data/Slice/InternalLemmas.olean +lib/lean/Init/Data/Slice/InternalLemmas.olean.private +lib/lean/Init/Data/Slice/InternalLemmas.olean.server lib/lean/Init/Data/Slice/Lemmas.ilean lib/lean/Init/Data/Slice/Lemmas.ir lib/lean/Init/Data/Slice/Lemmas.olean @@ -1677,11 +1828,26 @@ lib/lean/Init/Data/String/Extra.ir 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/Grind.ilean -lib/lean/Init/Data/String/Grind.ir -lib/lean/Init/Data/String/Grind.olean -lib/lean/Init/Data/String/Grind.olean.private -lib/lean/Init/Data/String/Grind.olean.server +lib/lean/Init/Data/String/FindPos.ilean +lib/lean/Init/Data/String/FindPos.ir +lib/lean/Init/Data/String/FindPos.olean +lib/lean/Init/Data/String/FindPos.olean.private +lib/lean/Init/Data/String/FindPos.olean.server +lib/lean/Init/Data/String/Hashable.ilean +lib/lean/Init/Data/String/Hashable.ir +lib/lean/Init/Data/String/Hashable.olean +lib/lean/Init/Data/String/Hashable.olean.private +lib/lean/Init/Data/String/Hashable.olean.server +lib/lean/Init/Data/String/Iter.ilean +lib/lean/Init/Data/String/Iter.ir +lib/lean/Init/Data/String/Iter.olean +lib/lean/Init/Data/String/Iter.olean.private +lib/lean/Init/Data/String/Iter.olean.server +lib/lean/Init/Data/String/Iterate.ilean +lib/lean/Init/Data/String/Iterate.ir +lib/lean/Init/Data/String/Iterate.olean +lib/lean/Init/Data/String/Iterate.olean.private +lib/lean/Init/Data/String/Iterate.olean.server lib/lean/Init/Data/String/Iterator.ilean lib/lean/Init/Data/String/Iterator.ir lib/lean/Init/Data/String/Iterator.olean @@ -1702,16 +1868,91 @@ lib/lean/Init/Data/String/Lemmas/Basic.ir lib/lean/Init/Data/String/Lemmas/Basic.olean lib/lean/Init/Data/String/Lemmas/Basic.olean.private lib/lean/Init/Data/String/Lemmas/Basic.olean.server +lib/lean/Init/Data/String/Lemmas/FindPos.ilean +lib/lean/Init/Data/String/Lemmas/FindPos.ir +lib/lean/Init/Data/String/Lemmas/FindPos.olean +lib/lean/Init/Data/String/Lemmas/FindPos.olean.private +lib/lean/Init/Data/String/Lemmas/FindPos.olean.server +lib/lean/Init/Data/String/Lemmas/IsEmpty.ilean +lib/lean/Init/Data/String/Lemmas/IsEmpty.ir +lib/lean/Init/Data/String/Lemmas/IsEmpty.olean +lib/lean/Init/Data/String/Lemmas/IsEmpty.olean.private +lib/lean/Init/Data/String/Lemmas/IsEmpty.olean.server +lib/lean/Init/Data/String/Lemmas/Iterate.ilean +lib/lean/Init/Data/String/Lemmas/Iterate.ir +lib/lean/Init/Data/String/Lemmas/Iterate.olean +lib/lean/Init/Data/String/Lemmas/Iterate.olean.private +lib/lean/Init/Data/String/Lemmas/Iterate.olean.server lib/lean/Init/Data/String/Lemmas/Modify.ilean lib/lean/Init/Data/String/Lemmas/Modify.ir lib/lean/Init/Data/String/Lemmas/Modify.olean lib/lean/Init/Data/String/Lemmas/Modify.olean.private lib/lean/Init/Data/String/Lemmas/Modify.olean.server +lib/lean/Init/Data/String/Lemmas/Order.ilean +lib/lean/Init/Data/String/Lemmas/Order.ir +lib/lean/Init/Data/String/Lemmas/Order.olean +lib/lean/Init/Data/String/Lemmas/Order.olean.private +lib/lean/Init/Data/String/Lemmas/Order.olean.server +lib/lean/Init/Data/String/Lemmas/Pattern.ilean +lib/lean/Init/Data/String/Lemmas/Pattern.ir +lib/lean/Init/Data/String/Lemmas/Pattern.olean +lib/lean/Init/Data/String/Lemmas/Pattern.olean.private +lib/lean/Init/Data/String/Lemmas/Pattern.olean.server +lib/lean/Init/Data/String/Lemmas/Pattern/Basic.ilean +lib/lean/Init/Data/String/Lemmas/Pattern/Basic.ir +lib/lean/Init/Data/String/Lemmas/Pattern/Basic.olean +lib/lean/Init/Data/String/Lemmas/Pattern/Basic.olean.private +lib/lean/Init/Data/String/Lemmas/Pattern/Basic.olean.server +lib/lean/Init/Data/String/Lemmas/Pattern/Char.ilean +lib/lean/Init/Data/String/Lemmas/Pattern/Char.ir +lib/lean/Init/Data/String/Lemmas/Pattern/Char.olean +lib/lean/Init/Data/String/Lemmas/Pattern/Char.olean.private +lib/lean/Init/Data/String/Lemmas/Pattern/Char.olean.server +lib/lean/Init/Data/String/Lemmas/Pattern/Memcmp.ilean +lib/lean/Init/Data/String/Lemmas/Pattern/Memcmp.ir +lib/lean/Init/Data/String/Lemmas/Pattern/Memcmp.olean +lib/lean/Init/Data/String/Lemmas/Pattern/Memcmp.olean.private +lib/lean/Init/Data/String/Lemmas/Pattern/Memcmp.olean.server +lib/lean/Init/Data/String/Lemmas/Pattern/Pred.ilean +lib/lean/Init/Data/String/Lemmas/Pattern/Pred.ir +lib/lean/Init/Data/String/Lemmas/Pattern/Pred.olean +lib/lean/Init/Data/String/Lemmas/Pattern/Pred.olean.private +lib/lean/Init/Data/String/Lemmas/Pattern/Pred.olean.server +lib/lean/Init/Data/String/Lemmas/Pattern/Split.ilean +lib/lean/Init/Data/String/Lemmas/Pattern/Split.ir +lib/lean/Init/Data/String/Lemmas/Pattern/Split.olean +lib/lean/Init/Data/String/Lemmas/Pattern/Split.olean.private +lib/lean/Init/Data/String/Lemmas/Pattern/Split.olean.server +lib/lean/Init/Data/String/Lemmas/Pattern/String.ilean +lib/lean/Init/Data/String/Lemmas/Pattern/String.ir +lib/lean/Init/Data/String/Lemmas/Pattern/String.olean +lib/lean/Init/Data/String/Lemmas/Pattern/String.olean.private +lib/lean/Init/Data/String/Lemmas/Pattern/String.olean.server +lib/lean/Init/Data/String/Lemmas/Pattern/String/Basic.ilean +lib/lean/Init/Data/String/Lemmas/Pattern/String/Basic.ir +lib/lean/Init/Data/String/Lemmas/Pattern/String/Basic.olean +lib/lean/Init/Data/String/Lemmas/Pattern/String/Basic.olean.private +lib/lean/Init/Data/String/Lemmas/Pattern/String/Basic.olean.server +lib/lean/Init/Data/String/Lemmas/Pattern/String/ForwardPattern.ilean +lib/lean/Init/Data/String/Lemmas/Pattern/String/ForwardPattern.ir +lib/lean/Init/Data/String/Lemmas/Pattern/String/ForwardPattern.olean +lib/lean/Init/Data/String/Lemmas/Pattern/String/ForwardPattern.olean.private +lib/lean/Init/Data/String/Lemmas/Pattern/String/ForwardPattern.olean.server +lib/lean/Init/Data/String/Lemmas/Pattern/String/ForwardSearcher.ilean +lib/lean/Init/Data/String/Lemmas/Pattern/String/ForwardSearcher.ir +lib/lean/Init/Data/String/Lemmas/Pattern/String/ForwardSearcher.olean +lib/lean/Init/Data/String/Lemmas/Pattern/String/ForwardSearcher.olean.private +lib/lean/Init/Data/String/Lemmas/Pattern/String/ForwardSearcher.olean.server lib/lean/Init/Data/String/Lemmas/Search.ilean lib/lean/Init/Data/String/Lemmas/Search.ir lib/lean/Init/Data/String/Lemmas/Search.olean lib/lean/Init/Data/String/Lemmas/Search.olean.private lib/lean/Init/Data/String/Lemmas/Search.olean.server +lib/lean/Init/Data/String/Lemmas/Slice.ilean +lib/lean/Init/Data/String/Lemmas/Slice.ir +lib/lean/Init/Data/String/Lemmas/Slice.olean +lib/lean/Init/Data/String/Lemmas/Slice.olean.private +lib/lean/Init/Data/String/Lemmas/Slice.olean.server lib/lean/Init/Data/String/Lemmas/Splits.ilean lib/lean/Init/Data/String/Lemmas/Splits.ir lib/lean/Init/Data/String/Lemmas/Splits.olean @@ -1722,6 +1963,11 @@ lib/lean/Init/Data/String/Modify.ir lib/lean/Init/Data/String/Modify.olean lib/lean/Init/Data/String/Modify.olean.private lib/lean/Init/Data/String/Modify.olean.server +lib/lean/Init/Data/String/OrderInstances.ilean +lib/lean/Init/Data/String/OrderInstances.ir +lib/lean/Init/Data/String/OrderInstances.olean +lib/lean/Init/Data/String/OrderInstances.olean.private +lib/lean/Init/Data/String/OrderInstances.olean.server lib/lean/Init/Data/String/Pattern.ilean lib/lean/Init/Data/String/Pattern.ir lib/lean/Init/Data/String/Pattern.olean @@ -1767,6 +2013,11 @@ lib/lean/Init/Data/String/Stream.ir lib/lean/Init/Data/String/Stream.olean lib/lean/Init/Data/String/Stream.olean.private lib/lean/Init/Data/String/Stream.olean.server +lib/lean/Init/Data/String/Subslice.ilean +lib/lean/Init/Data/String/Subslice.ir +lib/lean/Init/Data/String/Subslice.olean +lib/lean/Init/Data/String/Subslice.olean.private +lib/lean/Init/Data/String/Subslice.olean.server lib/lean/Init/Data/String/Substring.ilean lib/lean/Init/Data/String/Substring.ir lib/lean/Init/Data/String/Substring.olean @@ -1932,6 +2183,11 @@ lib/lean/Init/Data/Vector/InsertIdx.ir 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/Int.ilean +lib/lean/Init/Data/Vector/Int.ir +lib/lean/Init/Data/Vector/Int.olean +lib/lean/Init/Data/Vector/Int.olean.private +lib/lean/Init/Data/Vector/Int.olean.server lib/lean/Init/Data/Vector/Lemmas.ilean lib/lean/Init/Data/Vector/Lemmas.ir lib/lean/Init/Data/Vector/Lemmas.olean @@ -1952,6 +2208,11 @@ lib/lean/Init/Data/Vector/Monadic.ir 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/Nat.ilean +lib/lean/Init/Data/Vector/Nat.ir +lib/lean/Init/Data/Vector/Nat.olean +lib/lean/Init/Data/Vector/Nat.olean.private +lib/lean/Init/Data/Vector/Nat.olean.server lib/lean/Init/Data/Vector/OfFn.ilean lib/lean/Init/Data/Vector/OfFn.ir lib/lean/Init/Data/Vector/OfFn.olean @@ -2412,6 +2673,16 @@ lib/lean/Init/SizeOfLemmas.ir lib/lean/Init/SizeOfLemmas.olean lib/lean/Init/SizeOfLemmas.olean.private lib/lean/Init/SizeOfLemmas.olean.server +lib/lean/Init/Sym.ilean +lib/lean/Init/Sym.ir +lib/lean/Init/Sym.olean +lib/lean/Init/Sym.olean.private +lib/lean/Init/Sym.olean.server +lib/lean/Init/Sym/Lemmas.ilean +lib/lean/Init/Sym/Lemmas.ir +lib/lean/Init/Sym/Lemmas.olean +lib/lean/Init/Sym/Lemmas.olean.private +lib/lean/Init/Sym/Lemmas.olean.server lib/lean/Init/Syntax.ilean lib/lean/Init/Syntax.ir lib/lean/Init/Syntax.olean @@ -2487,6 +2758,16 @@ lib/lean/Init/WF.ir lib/lean/Init/WF.olean lib/lean/Init/WF.olean.private lib/lean/Init/WF.olean.server +lib/lean/Init/WFComputable.ilean +lib/lean/Init/WFComputable.ir +lib/lean/Init/WFComputable.olean +lib/lean/Init/WFComputable.olean.private +lib/lean/Init/WFComputable.olean.server +lib/lean/Init/WFExtrinsicFix.ilean +lib/lean/Init/WFExtrinsicFix.ir +lib/lean/Init/WFExtrinsicFix.olean +lib/lean/Init/WFExtrinsicFix.olean.private +lib/lean/Init/WFExtrinsicFix.olean.server lib/lean/Init/WFTactics.ilean lib/lean/Init/WFTactics.ir lib/lean/Init/WFTactics.olean @@ -2697,6 +2978,11 @@ lib/lean/Lake/CLI/Serve.ir lib/lean/Lake/CLI/Serve.olean lib/lean/Lake/CLI/Serve.olean.private lib/lean/Lake/CLI/Serve.olean.server +lib/lean/Lake/CLI/Shake.ilean +lib/lean/Lake/CLI/Shake.ir +lib/lean/Lake/CLI/Shake.olean +lib/lean/Lake/CLI/Shake.olean.private +lib/lean/Lake/CLI/Shake.olean.server lib/lean/Lake/CLI/Translate.ilean lib/lean/Lake/CLI/Translate.ir lib/lean/Lake/CLI/Translate.olean @@ -2802,6 +3088,11 @@ lib/lean/Lake/Config/Kinds.ir lib/lean/Lake/Config/Kinds.olean lib/lean/Lake/Config/Kinds.olean.private lib/lean/Lake/Config/Kinds.olean.server +lib/lean/Lake/Config/LakeConfig.ilean +lib/lean/Lake/Config/LakeConfig.ir +lib/lean/Lake/Config/LakeConfig.olean +lib/lean/Lake/Config/LakeConfig.olean.private +lib/lean/Lake/Config/LakeConfig.olean.server lib/lean/Lake/Config/Lang.ilean lib/lean/Lake/Config/Lang.ir lib/lean/Lake/Config/Lang.olean @@ -3357,16 +3648,6 @@ lib/lean/Lean/Compiler/IR/Basic.ir lib/lean/Lean/Compiler/IR/Basic.olean lib/lean/Lean/Compiler/IR/Basic.olean.private lib/lean/Lean/Compiler/IR/Basic.olean.server -lib/lean/Lean/Compiler/IR/Borrow.ilean -lib/lean/Lean/Compiler/IR/Borrow.ir -lib/lean/Lean/Compiler/IR/Borrow.olean -lib/lean/Lean/Compiler/IR/Borrow.olean.private -lib/lean/Lean/Compiler/IR/Borrow.olean.server -lib/lean/Lean/Compiler/IR/Boxing.ilean -lib/lean/Lean/Compiler/IR/Boxing.ir -lib/lean/Lean/Compiler/IR/Boxing.olean -lib/lean/Lean/Compiler/IR/Boxing.olean.private -lib/lean/Lean/Compiler/IR/Boxing.olean.server lib/lean/Lean/Compiler/IR/Checker.ilean lib/lean/Lean/Compiler/IR/Checker.ir lib/lean/Lean/Compiler/IR/Checker.olean @@ -3377,11 +3658,6 @@ lib/lean/Lean/Compiler/IR/CompilerM.ir lib/lean/Lean/Compiler/IR/CompilerM.olean lib/lean/Lean/Compiler/IR/CompilerM.olean.private lib/lean/Lean/Compiler/IR/CompilerM.olean.server -lib/lean/Lean/Compiler/IR/ElimDeadBranches.ilean -lib/lean/Lean/Compiler/IR/ElimDeadBranches.ir -lib/lean/Lean/Compiler/IR/ElimDeadBranches.olean -lib/lean/Lean/Compiler/IR/ElimDeadBranches.olean.private -lib/lean/Lean/Compiler/IR/ElimDeadBranches.olean.server lib/lean/Lean/Compiler/IR/ElimDeadVars.ilean lib/lean/Lean/Compiler/IR/ElimDeadVars.ir lib/lean/Lean/Compiler/IR/ElimDeadVars.olean @@ -3422,11 +3698,6 @@ lib/lean/Lean/Compiler/IR/LLVMBindings.ir lib/lean/Lean/Compiler/IR/LLVMBindings.olean lib/lean/Lean/Compiler/IR/LLVMBindings.olean.private lib/lean/Lean/Compiler/IR/LLVMBindings.olean.server -lib/lean/Lean/Compiler/IR/LiveVars.ilean -lib/lean/Lean/Compiler/IR/LiveVars.ir -lib/lean/Lean/Compiler/IR/LiveVars.olean -lib/lean/Lean/Compiler/IR/LiveVars.olean.private -lib/lean/Lean/Compiler/IR/LiveVars.olean.server lib/lean/Lean/Compiler/IR/Meta.ilean lib/lean/Lean/Compiler/IR/Meta.ir lib/lean/Lean/Compiler/IR/Meta.olean @@ -3442,21 +3713,16 @@ lib/lean/Lean/Compiler/IR/PushProj.ir lib/lean/Lean/Compiler/IR/PushProj.olean lib/lean/Lean/Compiler/IR/PushProj.olean.private lib/lean/Lean/Compiler/IR/PushProj.olean.server -lib/lean/Lean/Compiler/IR/RC.ilean -lib/lean/Lean/Compiler/IR/RC.ir -lib/lean/Lean/Compiler/IR/RC.olean -lib/lean/Lean/Compiler/IR/RC.olean.private -lib/lean/Lean/Compiler/IR/RC.olean.server -lib/lean/Lean/Compiler/IR/ResetReuse.ilean -lib/lean/Lean/Compiler/IR/ResetReuse.ir -lib/lean/Lean/Compiler/IR/ResetReuse.olean -lib/lean/Lean/Compiler/IR/ResetReuse.olean.private -lib/lean/Lean/Compiler/IR/ResetReuse.olean.server lib/lean/Lean/Compiler/IR/SimpCase.ilean lib/lean/Lean/Compiler/IR/SimpCase.ir lib/lean/Lean/Compiler/IR/SimpCase.olean lib/lean/Lean/Compiler/IR/SimpCase.olean.private lib/lean/Lean/Compiler/IR/SimpCase.olean.server +lib/lean/Lean/Compiler/IR/SimpleGroundExpr.ilean +lib/lean/Lean/Compiler/IR/SimpleGroundExpr.ir +lib/lean/Lean/Compiler/IR/SimpleGroundExpr.olean +lib/lean/Lean/Compiler/IR/SimpleGroundExpr.olean.private +lib/lean/Lean/Compiler/IR/SimpleGroundExpr.olean.server lib/lean/Lean/Compiler/IR/Sorry.ilean lib/lean/Lean/Compiler/IR/Sorry.ir lib/lean/Lean/Compiler/IR/Sorry.olean @@ -3472,11 +3738,6 @@ lib/lean/Lean/Compiler/IR/ToIRType.ir lib/lean/Lean/Compiler/IR/ToIRType.olean lib/lean/Lean/Compiler/IR/ToIRType.olean.private lib/lean/Lean/Compiler/IR/ToIRType.olean.server -lib/lean/Lean/Compiler/IR/Toposort.ilean -lib/lean/Lean/Compiler/IR/Toposort.ir -lib/lean/Lean/Compiler/IR/Toposort.olean -lib/lean/Lean/Compiler/IR/Toposort.olean.private -lib/lean/Lean/Compiler/IR/Toposort.olean.server lib/lean/Lean/Compiler/IR/UnboxResult.ilean lib/lean/Lean/Compiler/IR/UnboxResult.ir lib/lean/Lean/Compiler/IR/UnboxResult.olean @@ -3577,6 +3838,16 @@ lib/lean/Lean/Compiler/LCNF/ElimDeadBranches.ir lib/lean/Lean/Compiler/LCNF/ElimDeadBranches.olean *** 1991 LINES SKIPPED ***home | help
Want to link to this message? Use this
URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?69a14643.469ac.51d3da42>