Date: Tue, 26 May 2026 19:14:55 +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: 36ea07abaa7e - main - math/lean4: update 4.29.1=?utf-8?Q? =E2=86=92 4.3?=0.0 Message-ID: <6a15f12f.4516e.b326f54@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=36ea07abaa7eb36e6db092dcb7d01d3a986cf28f commit 36ea07abaa7eb36e6db092dcb7d01d3a986cf28f Author: Yuri Victorovich <yuri@FreeBSD.org> AuthorDate: 2026-05-26 19:13:56 +0000 Commit: Yuri Victorovich <yuri@FreeBSD.org> CommitDate: 2026-05-26 19:14:49 +0000 math/lean4: update 4.29.1 → 4.30.0 --- math/lean4/Makefile | 24 +- math/lean4/distinfo | 10 +- math/lean4/files/patch-src_CMakeLists.txt | 19 +- math/lean4/files/patch-src_runtime_io.cpp | 4 +- math/lean4/files/patch-stage0_src_CMakeLists.txt | 19 +- math/lean4/files/patch-tests_CMakeLists.txt | 18 + math/lean4/files/patch-tests_util.sh | 15 + math/lean4/pkg-plist | 22706 +++++++++++---------- 8 files changed, 11726 insertions(+), 11089 deletions(-) diff --git a/math/lean4/Makefile b/math/lean4/Makefile index 7e4ccae0b425..b3ea733ed160 100644 --- a/math/lean4/Makefile +++ b/math/lean4/Makefile @@ -1,6 +1,6 @@ PORTNAME= lean4 DISTVERSIONPREFIX= v -DISTVERSION= 4.29.1 +DISTVERSION= 4.30.0 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,6 +25,13 @@ USES= cmake:noninja,testing compiler:c++14-lang gmake pkgconfig python:build # USE_GITHUB= yes GH_ACCOUNT= leanprover +# leantar: a helper binary used by lake; fetched as a pre-built static linux binary +# (works on FreeBSD/amd64 and aarch64 as a statically-linked musl binary) +LEANTAR_VERSION= 0.1.19 +_LEANTAR_ARCH_amd64= x86_64-unknown-linux-musl +_LEANTAR_ARCH_aarch64= aarch64-unknown-linux-musl +MASTER_SITES_leantar= https://github.com/digama0/leangz/releases/download/v${LEANTAR_VERSION}/ + CFLAGS+= -fPIC CXXFLAGS+= -fPIC @@ -35,6 +42,14 @@ MAKE_ENV= LD_LIBRARY_PATH=${BUILD_WRKSRC}/stage0/lib/lean BINARY_ALIAS= make=${GMAKE} python=${PYTHON_CMD} +.include <bsd.port.pre.mk> + +.if defined(_LEANTAR_ARCH_${ARCH}) +LEANTAR_ARCH= ${_LEANTAR_ARCH_${ARCH}} +DISTFILES+= leantar-v${LEANTAR_VERSION}-${LEANTAR_ARCH}.tar.gz:leantar +CMAKE_ARGS+= -DLEANTAR=${WRKDIR}/leantar-v${LEANTAR_VERSION}-${LEANTAR_ARCH}/leantar +.endif + pre-everything:: @${ECHO_MSG} "" @${ECHO_MSG} "Please note that build Lean requires /proc to be mounted." @@ -50,7 +65,7 @@ post-patch: # Add weakLeancArgs = ["-fPIC"] to all test lakefile.toml files @${FIND} ${WRKSRC}/tests -name "lakefile.toml" | while read f; do \ ${GREP} -q "weakLeancArgs" "$$f" || \ - ( ${PRINTF} 'weakLeancArgs = ["-fPIC"]\n\n' | cat - "$$f" > "$$f.tmp" && ${MV} "$$f.tmp" "$$f" ); \ + ( ${PRINTF} 'weakLeancArgs = ["-fPIC"]\n\n' | ${CAT} - "$$f" > "$$f.tmp" && ${MV} "$$f.tmp" "$$f" ); \ done # Add weakLeancArgs to lakefile.lean files that define packages @${FIND} ${WRKSRC}/tests -name "lakefile.lean" | while read f; do \ @@ -71,14 +86,17 @@ post-install: bin/lake \ bin/lean \ bin/leanc \ + bin/leanir \ lib/lean/libInit_shared.so \ lib/lean/libleanshared.so \ lib/lean/libleanshared_1.so \ + lib/lean/libleanshared_2.so \ 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 # tests as of 4.29.0: 99% tests passed, 18 tests failed out of 3582, see https://github.com/leanprover/lean4/issues/13174 # tests as of 4.29.1: 99% tests passed, 24 tests failed out of 3584 +# tests as of 4.30.0: 100% tests passed, 0 tests failed out of 3678 -.include <bsd.port.mk> +.include <bsd.port.post.mk> diff --git a/math/lean4/distinfo b/math/lean4/distinfo index 3020aa5fab77..8945e10df2fc 100644 --- a/math/lean4/distinfo +++ b/math/lean4/distinfo @@ -1,3 +1,7 @@ -TIMESTAMP = 1776813893 -SHA256 (leanprover-lean4-v4.29.1_GH0.tar.gz) = 7a312f5c7e64233420b776cb9ba4ce05ed5c3d938bb3ed159cf69f892712e341 -SIZE (leanprover-lean4-v4.29.1_GH0.tar.gz) = 52782560 +TIMESTAMP = 1779810797 +SHA256 (leanprover-lean4-v4.30.0_GH0.tar.gz) = c11edd040d77be85865e41b4a37a77d14f824c07d8642434eb3561163f2afa5d +SIZE (leanprover-lean4-v4.30.0_GH0.tar.gz) = 70389698 +SHA256 (leantar-v0.1.19-aarch64-unknown-linux-musl.tar.gz) = 4f41a671bca685074dabef2dec5605c2431d177b471010f96ec322b5366136fe +SIZE (leantar-v0.1.19-aarch64-unknown-linux-musl.tar.gz) = 1105618 +SHA256 (leantar-v0.1.19-x86_64-unknown-linux-musl.tar.gz) = 81bb25e431791535597448f487e6a6321a1ba0c66e0846c07abc12adba139a39 +SIZE (leantar-v0.1.19-x86_64-unknown-linux-musl.tar.gz) = 1156919 diff --git a/math/lean4/files/patch-src_CMakeLists.txt b/math/lean4/files/patch-src_CMakeLists.txt index c7e42796fdc2..3bc5d1807f19 100644 --- a/math/lean4/files/patch-src_CMakeLists.txt +++ b/math/lean4/files/patch-src_CMakeLists.txt @@ -1,6 +1,15 @@ ---- src/CMakeLists.txt.orig 2026-02-24 00:20:30 UTC +--- src/CMakeLists.txt.orig 2026-05-26 08:34:15 UTC +++ src/CMakeLists.txt -@@ -517,7 +517,7 @@ endif() +@@ -384,7 +384,7 @@ endif() + endif() + endif() + +-include_directories(${CMAKE_BINARY_DIR}/include) ++include_directories(BEFORE ${CMAKE_BINARY_DIR}/include) + + # Pick up `llvm-config` to setup LLVM flags. + if(LLVM) +@@ -526,7 +526,7 @@ endif() string(APPEND LEAN_EXTRA_LINKER_FLAGS " -lm") endif() @@ -9,7 +18,7 @@ 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") +@@ -539,6 +539,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") @@ -29,7 +38,7 @@ 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") -@@ -653,6 +666,9 @@ string(APPEND LEANC_OPTS " -I${CMAKE_BINARY_DIR}/inclu +@@ -694,6 +707,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") @@ -39,7 +48,7 @@ # 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}}") -@@ -939,7 +955,7 @@ install( +@@ -1004,7 +1020,7 @@ install( install( DIRECTORY "${CMAKE_SOURCE_DIR}/" diff --git a/math/lean4/files/patch-src_runtime_io.cpp b/math/lean4/files/patch-src_runtime_io.cpp index 5f5125a68dc9..1bd0a5c504ba 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 2026-02-24 00:20:30 UTC +--- src/runtime/io.cpp.orig 2026-05-26 08:34:15 UTC +++ src/runtime/io.cpp -@@ -1390,7 +1390,13 @@ extern "C" LEAN_EXPORT obj_res lean_io_app_path() { +@@ -1396,7 +1396,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_CMakeLists.txt b/math/lean4/files/patch-stage0_src_CMakeLists.txt index b3e4a48d592e..9558ed1bbd8b 100644 --- a/math/lean4/files/patch-stage0_src_CMakeLists.txt +++ b/math/lean4/files/patch-stage0_src_CMakeLists.txt @@ -1,6 +1,15 @@ ---- stage0/src/CMakeLists.txt.orig 2026-02-24 00:20:30 UTC +--- stage0/src/CMakeLists.txt.orig 2026-05-26 08:34:15 UTC +++ stage0/src/CMakeLists.txt -@@ -517,7 +517,7 @@ endif() +@@ -384,7 +384,7 @@ endif() + endif() + endif() + +-include_directories(${CMAKE_BINARY_DIR}/include) ++include_directories(BEFORE ${CMAKE_BINARY_DIR}/include) + + # Pick up `llvm-config` to setup LLVM flags. + if(LLVM) +@@ -526,7 +526,7 @@ endif() string(APPEND LEAN_EXTRA_LINKER_FLAGS " -lm") endif() @@ -9,7 +18,7 @@ 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") +@@ -539,6 +539,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") @@ -29,7 +38,7 @@ 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") -@@ -653,6 +666,9 @@ string(APPEND LEANC_OPTS " -I${CMAKE_BINARY_DIR}/inclu +@@ -694,6 +707,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") @@ -39,7 +48,7 @@ # 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}}") -@@ -939,7 +955,7 @@ install( +@@ -1004,7 +1020,7 @@ install( install( DIRECTORY "${CMAKE_SOURCE_DIR}/" diff --git a/math/lean4/files/patch-tests_CMakeLists.txt b/math/lean4/files/patch-tests_CMakeLists.txt new file mode 100644 index 000000000000..ef5c1dceb35c --- /dev/null +++ b/math/lean4/files/patch-tests_CMakeLists.txt @@ -0,0 +1,18 @@ +-- Add LD_LIBRARY_PATH to the test environment on FreeBSD/Linux. +-- Lake-built shared objects have no RPATH embedded, so the dynamic linker cannot +-- find libLake_shared.so at test runtime without LD_LIBRARY_PATH. +--- tests/CMakeLists.txt.orig 2026-05-26 17:39:45 UTC ++++ tests/CMakeLists.txt +@@ -38,6 +38,12 @@ string(APPEND TEST_VARS " CXX='${CMAKE_CXX_COMPILER} $ + # LEANC_OPTS in CXX is necessary for macOS c++ to find its headers + string(APPEND TEST_VARS " CXX='${CMAKE_CXX_COMPILER} ${LEANC_OPTS}'") + ++# FreeBSD/Linux: lake-built shared objects have no rpath embedded, so we need ++# LD_LIBRARY_PATH to find libLake_shared.so and other lean shared libs at test runtime. ++if(CMAKE_SYSTEM_NAME MATCHES "FreeBSD|Linux") ++ string(APPEND TEST_VARS " LD_LIBRARY_PATH='${MANGLED_BINARY_DIR}/lib/lean'") ++endif() ++ + set(WITH_TEST_ENV "${CMAKE_CURRENT_SOURCE_DIR}/with_stage${STAGE}_test_env.sh") + set(WITH_BENCH_ENV "${CMAKE_CURRENT_SOURCE_DIR}/with_stage${STAGE}_bench_env.sh") + diff --git a/math/lean4/files/patch-tests_util.sh b/math/lean4/files/patch-tests_util.sh new file mode 100644 index 000000000000..8252d4c23b2c --- /dev/null +++ b/math/lean4/files/patch-tests_util.sh @@ -0,0 +1,15 @@ +-- Fix mktemp usage to be compatible with FreeBSD. +-- FreeBSD's mktemp does not support --tmpdir/--directory flags the same way +-- GNU coreutils does; on FreeBSD those flags create the directory in CWD and +-- return a relative path, which breaks tests that pushd into subdirectories. +--- tests/util.sh.orig 2026-05-26 18:04:51 UTC ++++ tests/util.sh +@@ -5,7 +5,7 @@ DIFF="diff -au --strip-trailing-cr --color=always" + DIFF="diff -au --strip-trailing-cr --color=always" + + # Temporary directory to store unnamed output files +-TMP_DIR="$(mktemp --tmpdir --directory lean4-test-suite.XXXXXXXXXX)" ++TMP_DIR="$(mktemp -d "${TMPDIR:-/tmp}/lean4-test-suite.XXXXXXXXXX")" + trap 'rm -rf "$TMP_DIR"' EXIT + + function fail { diff --git a/math/lean4/pkg-plist b/math/lean4/pkg-plist index 23477d679820..cf3c31bf4df4 100644 --- a/math/lean4/pkg-plist +++ b/math/lean4/pkg-plist @@ -1,11068 +1,8 @@ -bin/lake -bin/lean -bin/leanc -bin/leanchecker -bin/leanmake -include/lean/config.h -include/lean/lean.h -include/lean/lean_gmp.h -include/lean/lean_libuv.h -include/lean/version.h -lib/lean/Init.ilean -lib/lean/Init.ir -lib/lean/Init.olean -lib/lean/Init.olean.private -lib/lean/Init.olean.server -lib/lean/Init/BinderNameHint.ilean -lib/lean/Init/BinderNameHint.ir -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.ir -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.ir -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.ir -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.ir -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.ir -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.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 -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.ir -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.ir -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.ir -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.ir -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.ir -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.ir -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.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 -lib/lean/Init/Control/Lawful/MonadLift.olean.private -lib/lean/Init/Control/Lawful/MonadLift.olean.server -lib/lean/Init/Control/Lawful/MonadLift/Basic.ilean -lib/lean/Init/Control/Lawful/MonadLift/Basic.ir -lib/lean/Init/Control/Lawful/MonadLift/Basic.olean -lib/lean/Init/Control/Lawful/MonadLift/Basic.olean.private -lib/lean/Init/Control/Lawful/MonadLift/Basic.olean.server -lib/lean/Init/Control/Lawful/MonadLift/Instances.ilean -lib/lean/Init/Control/Lawful/MonadLift/Instances.ir -lib/lean/Init/Control/Lawful/MonadLift/Instances.olean -lib/lean/Init/Control/Lawful/MonadLift/Instances.olean.private -lib/lean/Init/Control/Lawful/MonadLift/Instances.olean.server -lib/lean/Init/Control/Lawful/MonadLift/Lemmas.ilean -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 -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.ir -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.ir -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.ir -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.ir -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.ir -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.ir -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.ir -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.ir -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.ir -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.ir -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.ir -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.ir -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.ir -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.ir -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.ir -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.ir -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.ir -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.ir -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.ir -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.ir -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.ir -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.ir -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.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 -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.ir -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.ir -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.ir -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.ir -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.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 -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.ir -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.ir -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.ir -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.ir -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.ir -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.ir -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.ir -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.ir -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.ir -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.ir -lib/lean/Init/Data/BEq.olean -lib/lean/Init/Data/BEq.olean.private -lib/lean/Init/Data/BEq.olean.server -lib/lean/Init/Data/BitVec.ilean -lib/lean/Init/Data/BitVec.ir -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.ir -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.ir -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.ir -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/Bootstrap.ilean -lib/lean/Init/Data/BitVec/Bootstrap.ir -lib/lean/Init/Data/BitVec/Bootstrap.olean -lib/lean/Init/Data/BitVec/Bootstrap.olean.private -lib/lean/Init/Data/BitVec/Bootstrap.olean.server -lib/lean/Init/Data/BitVec/Decidable.ilean -lib/lean/Init/Data/BitVec/Decidable.ir -lib/lean/Init/Data/BitVec/Decidable.olean -lib/lean/Init/Data/BitVec/Decidable.olean.private -lib/lean/Init/Data/BitVec/Decidable.olean.server -lib/lean/Init/Data/BitVec/Folds.ilean -lib/lean/Init/Data/BitVec/Folds.ir -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.ir -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.ir -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.ir -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.ir -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/ByteArray/Bootstrap.ilean -lib/lean/Init/Data/ByteArray/Bootstrap.ir -lib/lean/Init/Data/ByteArray/Bootstrap.olean -lib/lean/Init/Data/ByteArray/Bootstrap.olean.private -lib/lean/Init/Data/ByteArray/Bootstrap.olean.server -lib/lean/Init/Data/ByteArray/Extra.ilean -lib/lean/Init/Data/ByteArray/Extra.ir -lib/lean/Init/Data/ByteArray/Extra.olean -lib/lean/Init/Data/ByteArray/Extra.olean.private -lib/lean/Init/Data/ByteArray/Extra.olean.server -lib/lean/Init/Data/ByteArray/Lemmas.ilean -lib/lean/Init/Data/ByteArray/Lemmas.ir -lib/lean/Init/Data/ByteArray/Lemmas.olean -lib/lean/Init/Data/ByteArray/Lemmas.olean.private -lib/lean/Init/Data/ByteArray/Lemmas.olean.server -lib/lean/Init/Data/Cast.ilean -lib/lean/Init/Data/Cast.ir -lib/lean/Init/Data/Cast.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.ir -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.ir -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.ir -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/Char/Order.ilean -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 -lib/lean/Init/Data/Dyadic.olean.private -lib/lean/Init/Data/Dyadic.olean.server -lib/lean/Init/Data/Dyadic/Basic.ilean -lib/lean/Init/Data/Dyadic/Basic.ir -lib/lean/Init/Data/Dyadic/Basic.olean -lib/lean/Init/Data/Dyadic/Basic.olean.private -lib/lean/Init/Data/Dyadic/Basic.olean.server -lib/lean/Init/Data/Dyadic/Instances.ilean -lib/lean/Init/Data/Dyadic/Instances.ir -lib/lean/Init/Data/Dyadic/Instances.olean -lib/lean/Init/Data/Dyadic/Instances.olean.private -lib/lean/Init/Data/Dyadic/Instances.olean.server -lib/lean/Init/Data/Dyadic/Inv.ilean -lib/lean/Init/Data/Dyadic/Inv.ir -lib/lean/Init/Data/Dyadic/Inv.olean -lib/lean/Init/Data/Dyadic/Inv.olean.private -lib/lean/Init/Data/Dyadic/Inv.olean.server -lib/lean/Init/Data/Dyadic/Round.ilean -lib/lean/Init/Data/Dyadic/Round.ir -lib/lean/Init/Data/Dyadic/Round.olean -lib/lean/Init/Data/Dyadic/Round.olean.private -lib/lean/Init/Data/Dyadic/Round.olean.server -lib/lean/Init/Data/Fin.ilean -lib/lean/Init/Data/Fin.ir -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.ir -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.ir -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.ir -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.ir -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.ir -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.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 -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.ir -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.ir -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.ir -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.ir -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.ir -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.ir -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.ir -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.ir -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.ir -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.ir -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.ir -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.ir -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.ir -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.ir -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.ir -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.ir -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.ir -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.ir -lib/lean/Init/Data/Int/DivMod.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.ir -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.ir -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.ir -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/DivMod/Pow.ilean -lib/lean/Init/Data/Int/DivMod/Pow.ir -lib/lean/Init/Data/Int/DivMod/Pow.olean -lib/lean/Init/Data/Int/DivMod/Pow.olean.private -lib/lean/Init/Data/Int/DivMod/Pow.olean.server -lib/lean/Init/Data/Int/Gcd.ilean -lib/lean/Init/Data/Int/Gcd.ir -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.ir -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.ir -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.ir -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.ir -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.ir -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.ir -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/Iterators.ilean -lib/lean/Init/Data/Iterators.ir -lib/lean/Init/Data/Iterators.olean -lib/lean/Init/Data/Iterators.olean.private -lib/lean/Init/Data/Iterators.olean.server -lib/lean/Init/Data/Iterators/Basic.ilean -lib/lean/Init/Data/Iterators/Basic.ir -lib/lean/Init/Data/Iterators/Basic.olean -lib/lean/Init/Data/Iterators/Basic.olean.private -lib/lean/Init/Data/Iterators/Basic.olean.server -lib/lean/Init/Data/Iterators/Combinators.ilean -lib/lean/Init/Data/Iterators/Combinators.ir -lib/lean/Init/Data/Iterators/Combinators.olean -lib/lean/Init/Data/Iterators/Combinators.olean.private -lib/lean/Init/Data/Iterators/Combinators.olean.server -lib/lean/Init/Data/Iterators/Combinators/Attach.ilean -lib/lean/Init/Data/Iterators/Combinators/Attach.ir -lib/lean/Init/Data/Iterators/Combinators/Attach.olean -lib/lean/Init/Data/Iterators/Combinators/Attach.olean.private -lib/lean/Init/Data/Iterators/Combinators/Attach.olean.server -lib/lean/Init/Data/Iterators/Combinators/FilterMap.ilean -lib/lean/Init/Data/Iterators/Combinators/FilterMap.ir -lib/lean/Init/Data/Iterators/Combinators/FilterMap.olean -lib/lean/Init/Data/Iterators/Combinators/FilterMap.olean.private -lib/lean/Init/Data/Iterators/Combinators/FilterMap.olean.server -lib/lean/Init/Data/Iterators/Combinators/FlatMap.ilean -lib/lean/Init/Data/Iterators/Combinators/FlatMap.ir -lib/lean/Init/Data/Iterators/Combinators/FlatMap.olean -lib/lean/Init/Data/Iterators/Combinators/FlatMap.olean.private -lib/lean/Init/Data/Iterators/Combinators/FlatMap.olean.server -lib/lean/Init/Data/Iterators/Combinators/Monadic.ilean -lib/lean/Init/Data/Iterators/Combinators/Monadic.ir -lib/lean/Init/Data/Iterators/Combinators/Monadic.olean -lib/lean/Init/Data/Iterators/Combinators/Monadic.olean.private -lib/lean/Init/Data/Iterators/Combinators/Monadic.olean.server -lib/lean/Init/Data/Iterators/Combinators/Monadic/Attach.ilean -lib/lean/Init/Data/Iterators/Combinators/Monadic/Attach.ir -lib/lean/Init/Data/Iterators/Combinators/Monadic/Attach.olean -lib/lean/Init/Data/Iterators/Combinators/Monadic/Attach.olean.private -lib/lean/Init/Data/Iterators/Combinators/Monadic/Attach.olean.server -lib/lean/Init/Data/Iterators/Combinators/Monadic/FilterMap.ilean -lib/lean/Init/Data/Iterators/Combinators/Monadic/FilterMap.ir -lib/lean/Init/Data/Iterators/Combinators/Monadic/FilterMap.olean -lib/lean/Init/Data/Iterators/Combinators/Monadic/FilterMap.olean.private -lib/lean/Init/Data/Iterators/Combinators/Monadic/FilterMap.olean.server *** 22272 LINES SKIPPED ***home | help
Want to link to this message? Use this
URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?6a15f12f.4516e.b326f54>