git: 6dd0fb54cd6c - main - math/lean4: update 4.32.1 → 4.33.1
- Go to: [ bottom of page ] [ top of archives ] [ this month ]
Date: Sun, 06 Sep 2026 06:19:02 UTC
The branch main has been updated by yuri:
URL: https://cgit.FreeBSD.org/ports/commit/?id=6dd0fb54cd6ce538fccd4e3d5eafff4740cffff9
commit 6dd0fb54cd6ce538fccd4e3d5eafff4740cffff9
Author: Yuri Victorovich <yuri@FreeBSD.org>
AuthorDate: 2026-09-05 04:00:50 +0000
Commit: Yuri Victorovich <yuri@FreeBSD.org>
CommitDate: 2026-09-06 06:18:25 +0000
math/lean4: update 4.32.1 → 4.33.1
---
math/lean4/Makefile | 21 +-
math/lean4/distinfo | 6 +-
math/lean4/files/patch-tests_CMakeLists.txt | 37 +-
.../lean4/files/patch-tests_lake_tests_old_test.sh | 43 +
math/lean4/pkg-plist | 2855 +++++++++++++++++++-
5 files changed, 2913 insertions(+), 49 deletions(-)
diff --git a/math/lean4/Makefile b/math/lean4/Makefile
index 3d910dcc99ed..ea8cdf9106b7 100644
--- a/math/lean4/Makefile
+++ b/math/lean4/Makefile
@@ -1,6 +1,6 @@
PORTNAME= lean4
DISTVERSIONPREFIX= v
-DISTVERSION= 4.32.1
+DISTVERSION= 4.33.1
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
@@ -16,14 +16,12 @@ BROKEN_i386= linking fails: INTERNAL PANIC: out of memory (during: Linking runLi
BUILD_DEPENDS= bash:shells/bash \
cadical:math/cadical \
- gsed:textproc/gsed \
leantar:math/leangz
LIB_DEPENDS= libgmp.so:math/gmp \
libuv.so:devel/libuv
RUN_DEPENDS= cadical:math/cadical \
leantar:math/leangz
-TEST_DEPENDS= gtail:sysutils/coreutils \
- gsed:textproc/gsed
+TEST_DEPENDS= gtail:sysutils/coreutils
USES= cmake:noninja,testing compiler:c++14-lang gmake pkgconfig python:build # ninja fails + gmake scripts are included in the project
@@ -41,15 +39,20 @@ MAKE_ENV= LD_LIBRARY_PATH=${BUILD_WRKSRC}/stage0/lib/lean
BINARY_ALIAS= make=${GMAKE} \
python=${PYTHON_CMD} \
- sed=${LOCALBASE}/bin/gsed
+ python3=${PYTHON_CMD}
CMAKE_ARGS+= -DLEANTAR=${LOCALBASE}/bin/leantar
+CONFLICTS_BUILD= gsed # this should be CONFLICTS_TEST but it isn't defined; pesence of gsed for some reason makes several tests fail
+
post-configure:
# Copy leantar to build bin directories for tests (INSTALL_LEANTAR=OFF disables the built-in copy)
@${MKDIR} ${BUILD_WRKSRC}/stage0/bin ${BUILD_WRKSRC}/stage1/bin
@${CP} ${LOCALBASE}/bin/leantar ${BUILD_WRKSRC}/stage0/bin/
@${CP} ${LOCALBASE}/bin/leantar ${BUILD_WRKSRC}/stage1/bin/
+ # Create a test-only bin dir with gmake as "make" for tests needing GNU make (e.g. reverse-ffi) (need to see why BINARY ALIAS doesn't work for this)
+ @${MKDIR} ${BUILD_WRKSRC}/test-bin
+ @${LN} -sf ${LOCALBASE}/bin/gmake ${BUILD_WRKSRC}/test-bin/make
pre-everything::
@${ECHO_MSG} ""
@@ -97,12 +100,6 @@ post-install:
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
-# tests as of 4.31.0: 99% tests passed, 2 tests failed out of 3858
-# 2 failures are not port issues: cache/test.sh, ltar/test.sh: leantar panic (math/leangz bug, see reproducer-leangz/)
+# tests as of 4.33.1: 100% tests passed, 0 tests failed out of 3988
.include <bsd.port.mk>
diff --git a/math/lean4/distinfo b/math/lean4/distinfo
index f98762b632d4..a0cba28f01b4 100644
--- a/math/lean4/distinfo
+++ b/math/lean4/distinfo
@@ -1,3 +1,3 @@
-TIMESTAMP = 1785103908
-SHA256 (leanprover-lean4-v4.32.1_GH0.tar.gz) = 5ee893d6081dba103c3d1206930a0637f9dd8afe3c631823b98a21593386dbd7
-SIZE (leanprover-lean4-v4.32.1_GH0.tar.gz) = 75094335
+TIMESTAMP = 1788581049
+SHA256 (leanprover-lean4-v4.33.1_GH0.tar.gz) = 561b500da16419aec0baeba5dc47ad11979b5bdcd30a02aafc88c3eed599b766
+SIZE (leanprover-lean4-v4.33.1_GH0.tar.gz) = 86700313
diff --git a/math/lean4/files/patch-tests_CMakeLists.txt b/math/lean4/files/patch-tests_CMakeLists.txt
index ef5c1dceb35c..9589cbd73125 100644
--- a/math/lean4/files/patch-tests_CMakeLists.txt
+++ b/math/lean4/files/patch-tests_CMakeLists.txt
@@ -1,11 +1,31 @@
-- 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
+
+-- On FreeBSD, prepend a test-bin directory (containing a 'make' symlink to gmake)
+-- to PATH so that tests using GNU make syntax (e.g. reverse-ffi) work correctly.
+
+-- Disable the lint.py test because it calls git to find the list of tracked files to lint.
+
+--- tests/CMakeLists.txt.orig 2026-08-21 10:26:01 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}'")
+@@ -21,6 +21,13 @@ endif()
+
+ set(LEAN_BIN "${MANGLED_BINARY_DIR}/bin")
+
++# FreeBSD: prepend test-bin (contains 'make' -> gmake symlink) to PATH so that tests
++# using GNU make syntax (e.g. reverse-ffi) work correctly with FreeBSD's BSD make.
++if(CMAKE_SYSTEM_NAME MATCHES "FreeBSD")
++ get_filename_component(TEST_BIN_DIR "${CMAKE_BINARY_DIR}" DIRECTORY)
++ set(LEAN_BIN "'${TEST_BIN_DIR}/test-bin':'${MANGLED_BINARY_DIR}/bin'")
++endif()
++
+ # Use the current stage's lean binary instead of whatever lake thinks we want
+ string(APPEND TEST_VARS " PATH='${LEAN_BIN}':\"$PATH\"")
+
+@@ -51,6 +58,12 @@ endif()
+ string(APPEND TEST_VARS " LEAN_HEADER_SNAPSHOT_INIT='${MANGLED_CURRENT_BINARY_DIR}/lean_header_init.snap'")
+ endif()
+# 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.
@@ -16,3 +36,12 @@
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")
+@@ -309,7 +322,7 @@ endforeach(T)
+ endforeach(T)
+
+ # Lint test suite and parts of the repository.
+-add_test(NAME lint.py COMMAND python3 lint.py WORKING_DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR}")
++#add_test(NAME lint.py COMMAND python3 lint.py WORKING_DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR}")
+
+ add_test_pile(../doc/examples *.lean)
+ add_test_pile(compile *.lean BENCH PART2)
diff --git a/math/lean4/files/patch-tests_lake_tests_old_test.sh b/math/lean4/files/patch-tests_lake_tests_old_test.sh
new file mode 100644
index 000000000000..b74dece65020
--- /dev/null
+++ b/math/lean4/files/patch-tests_lake_tests_old_test.sh
@@ -0,0 +1,43 @@
+-- Make old Lake test portable and non-hanging on FreeBSD.
+-- BSD sed does not support `\s`, so use a POSIX character class. Also group
+-- `grep ... || true` before piping so process substitution FIFOs are always read.
+-- Update expected "Built ..." lines to the Lean 4.33.1 output format.
+
+--- tests/lake/tests/old/test.sh.orig 2026-08-21 10:26:01 UTC
++++ tests/lake/tests/old/test.sh
+@@ -10,9 +10,9 @@ diff_out() {
+ # https://github.com/leanprover/lean4/issues/2822
+
+ diff_out() {
+- grep 'Built' || true |
++ { grep 'Built' || true; } |
+ sed 's/^.*\[.*\] //' |
+- sed 's/\s*(.*)$//' |
++ sed -E 's/[[:space:]]*(\(.*\))$//' |
+ LANG=POSIX sort |
+ diff -u --strip-trailing-cr "$1" -
+ }
+@@ -25,8 +25,8 @@ Built Hello.Basic
+ echo 'def hello := "old"' > hello/Hello/Basic.lean
+ $LAKE -d hello build --old | diff_out <(cat << 'EOF'
+ Built Hello.Basic
+-Built Hello.Basic:c
+-Built hello
++Built Hello.Basic:c.o
++Built hello:exe
+ EOF
+ )
+
+@@ -35,9 +35,10 @@ Built Hello.Basic
+ $LAKE -d hello build | diff_out <(cat << 'EOF'
+ Built Hello
+ Built Hello.Basic
+-Built Hello.Basic:c
++Built Hello.Basic:c.o
+ Built Main
+-Built hello
++Built Main:c.o
++Built hello:exe
+ EOF
+ )
+
diff --git a/math/lean4/pkg-plist b/math/lean4/pkg-plist
index 457a48e72b63..595da85c500f 100644
--- a/math/lean4/pkg-plist
+++ b/math/lean4/pkg-plist
@@ -11,9771 +11,11995 @@ include/lean/lean_libuv.h
include/lean/version.h
lib/lean/Init.ilean
lib/lean/Init.ir
+lib/lean/Init.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
lib/lean/Init/ByCases.olean
lib/lean/Init/ByCases.olean.private
lib/lean/Init/ByCases.olean.server
lib/lean/Init/CbvSimproc.ilean
lib/lean/Init/CbvSimproc.ir
+lib/lean/Init/CbvSimproc.ir.sig
lib/lean/Init/CbvSimproc.olean
lib/lean/Init/CbvSimproc.olean.private
lib/lean/Init/CbvSimproc.olean.server
lib/lean/Init/Classical.ilean
lib/lean/Init/Classical.ir
+lib/lean/Init/Classical.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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/Sort.ilean
lib/lean/Init/Data/Array/Sort.ir
+lib/lean/Init/Data/Array/Sort.ir.sig
lib/lean/Init/Data/Array/Sort.olean
lib/lean/Init/Data/Array/Sort.olean.private
lib/lean/Init/Data/Array/Sort.olean.server
lib/lean/Init/Data/Array/Sort/Basic.ilean
lib/lean/Init/Data/Array/Sort/Basic.ir
+lib/lean/Init/Data/Array/Sort/Basic.ir.sig
lib/lean/Init/Data/Array/Sort/Basic.olean
lib/lean/Init/Data/Array/Sort/Basic.olean.private
lib/lean/Init/Data/Array/Sort/Basic.olean.server
lib/lean/Init/Data/Array/Sort/Lemmas.ilean
lib/lean/Init/Data/Array/Sort/Lemmas.ir
+lib/lean/Init/Data/Array/Sort/Lemmas.ir.sig
lib/lean/Init/Data/Array/Sort/Lemmas.olean
lib/lean/Init/Data/Array/Sort/Lemmas.olean.private
lib/lean/Init/Data/Array/Sort/Lemmas.olean.server
lib/lean/Init/Data/Array/Subarray.ilean
lib/lean/Init/Data/Array/Subarray.ir
+lib/lean/Init/Data/Array/Subarray.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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.ir.sig
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/Float/Float.ilean
+lib/lean/Init/Data/Float/Float.ir
+lib/lean/Init/Data/Float/Float.ir.sig
+lib/lean/Init/Data/Float/Float.olean
+lib/lean/Init/Data/Float/Float.olean.private
+lib/lean/Init/Data/Float/Float.olean.server
+lib/lean/Init/Data/Float/Float32.ilean
+lib/lean/Init/Data/Float/Float32.ir
+lib/lean/Init/Data/Float/Float32.ir.sig
+lib/lean/Init/Data/Float/Float32.olean
+lib/lean/Init/Data/Float/Float32.olean.private
+lib/lean/Init/Data/Float/Float32.olean.server
+lib/lean/Init/Data/Float/Model.ilean
+lib/lean/Init/Data/Float/Model.ir
+lib/lean/Init/Data/Float/Model.ir.sig
+lib/lean/Init/Data/Float/Model.olean
+lib/lean/Init/Data/Float/Model.olean.private
+lib/lean/Init/Data/Float/Model.olean.server
+lib/lean/Init/Data/Float/Model/Float.ilean
+lib/lean/Init/Data/Float/Model/Float.ir
+lib/lean/Init/Data/Float/Model/Float.ir.sig
+lib/lean/Init/Data/Float/Model/Float.olean
+lib/lean/Init/Data/Float/Model/Float.olean.private
+lib/lean/Init/Data/Float/Model/Float.olean.server
+lib/lean/Init/Data/Float/Model/Float32.ilean
+lib/lean/Init/Data/Float/Model/Float32.ir
+lib/lean/Init/Data/Float/Model/Float32.ir.sig
+lib/lean/Init/Data/Float/Model/Float32.olean
+lib/lean/Init/Data/Float/Model/Float32.olean.private
+lib/lean/Init/Data/Float/Model/Float32.olean.server
+lib/lean/Init/Data/Float/Model/Format.ilean
+lib/lean/Init/Data/Float/Model/Format.ir
+lib/lean/Init/Data/Float/Model/Format.ir.sig
+lib/lean/Init/Data/Float/Model/Format.olean
+lib/lean/Init/Data/Float/Model/Format.olean.private
+lib/lean/Init/Data/Float/Model/Format.olean.server
+lib/lean/Init/Data/Float/Model/Format/Basic.ilean
+lib/lean/Init/Data/Float/Model/Format/Basic.ir
+lib/lean/Init/Data/Float/Model/Format/Basic.ir.sig
+lib/lean/Init/Data/Float/Model/Format/Basic.olean
+lib/lean/Init/Data/Float/Model/Format/Basic.olean.private
+lib/lean/Init/Data/Float/Model/Format/Basic.olean.server
+lib/lean/Init/Data/Float/Model/Format/Valid.ilean
+lib/lean/Init/Data/Float/Model/Format/Valid.ir
+lib/lean/Init/Data/Float/Model/Format/Valid.ir.sig
+lib/lean/Init/Data/Float/Model/Format/Valid.olean
+lib/lean/Init/Data/Float/Model/Format/Valid.olean.private
+lib/lean/Init/Data/Float/Model/Format/Valid.olean.server
+lib/lean/Init/Data/Float/Model/Unpacked.ilean
+lib/lean/Init/Data/Float/Model/Unpacked.ir
+lib/lean/Init/Data/Float/Model/Unpacked.ir.sig
+lib/lean/Init/Data/Float/Model/Unpacked.olean
+lib/lean/Init/Data/Float/Model/Unpacked.olean.private
+lib/lean/Init/Data/Float/Model/Unpacked.olean.server
+lib/lean/Init/Data/Float/Model/Unpacked/Basic.ilean
+lib/lean/Init/Data/Float/Model/Unpacked/Basic.ir
+lib/lean/Init/Data/Float/Model/Unpacked/Basic.ir.sig
+lib/lean/Init/Data/Float/Model/Unpacked/Basic.olean
+lib/lean/Init/Data/Float/Model/Unpacked/Basic.olean.private
+lib/lean/Init/Data/Float/Model/Unpacked/Basic.olean.server
+lib/lean/Init/Data/Float/Model/Unpacked/Operations.ilean
+lib/lean/Init/Data/Float/Model/Unpacked/Operations.ir
+lib/lean/Init/Data/Float/Model/Unpacked/Operations.ir.sig
+lib/lean/Init/Data/Float/Model/Unpacked/Operations.olean
+lib/lean/Init/Data/Float/Model/Unpacked/Operations.olean.private
+lib/lean/Init/Data/Float/Model/Unpacked/Operations.olean.server
+lib/lean/Init/Data/Float/Model/Unpacked/Operations/Add.ilean
+lib/lean/Init/Data/Float/Model/Unpacked/Operations/Add.ir
+lib/lean/Init/Data/Float/Model/Unpacked/Operations/Add.ir.sig
+lib/lean/Init/Data/Float/Model/Unpacked/Operations/Add.olean
+lib/lean/Init/Data/Float/Model/Unpacked/Operations/Add.olean.private
+lib/lean/Init/Data/Float/Model/Unpacked/Operations/Add.olean.server
+lib/lean/Init/Data/Float/Model/Unpacked/Operations/Compare.ilean
+lib/lean/Init/Data/Float/Model/Unpacked/Operations/Compare.ir
+lib/lean/Init/Data/Float/Model/Unpacked/Operations/Compare.ir.sig
+lib/lean/Init/Data/Float/Model/Unpacked/Operations/Compare.olean
+lib/lean/Init/Data/Float/Model/Unpacked/Operations/Compare.olean.private
+lib/lean/Init/Data/Float/Model/Unpacked/Operations/Compare.olean.server
+lib/lean/Init/Data/Float/Model/Unpacked/Operations/Div.ilean
+lib/lean/Init/Data/Float/Model/Unpacked/Operations/Div.ir
+lib/lean/Init/Data/Float/Model/Unpacked/Operations/Div.ir.sig
+lib/lean/Init/Data/Float/Model/Unpacked/Operations/Div.olean
+lib/lean/Init/Data/Float/Model/Unpacked/Operations/Div.olean.private
+lib/lean/Init/Data/Float/Model/Unpacked/Operations/Div.olean.server
+lib/lean/Init/Data/Float/Model/Unpacked/Operations/Mul.ilean
+lib/lean/Init/Data/Float/Model/Unpacked/Operations/Mul.ir
+lib/lean/Init/Data/Float/Model/Unpacked/Operations/Mul.ir.sig
+lib/lean/Init/Data/Float/Model/Unpacked/Operations/Mul.olean
+lib/lean/Init/Data/Float/Model/Unpacked/Operations/Mul.olean.private
+lib/lean/Init/Data/Float/Model/Unpacked/Operations/Mul.olean.server
+lib/lean/Init/Data/Float/Model/Unpacked/Operations/OfNat.ilean
+lib/lean/Init/Data/Float/Model/Unpacked/Operations/OfNat.ir
+lib/lean/Init/Data/Float/Model/Unpacked/Operations/OfNat.ir.sig
+lib/lean/Init/Data/Float/Model/Unpacked/Operations/OfNat.olean
+lib/lean/Init/Data/Float/Model/Unpacked/Operations/OfNat.olean.private
+lib/lean/Init/Data/Float/Model/Unpacked/Operations/OfNat.olean.server
+lib/lean/Init/Data/Float/Model/Unpacked/Operations/OfScientific.ilean
+lib/lean/Init/Data/Float/Model/Unpacked/Operations/OfScientific.ir
+lib/lean/Init/Data/Float/Model/Unpacked/Operations/OfScientific.ir.sig
+lib/lean/Init/Data/Float/Model/Unpacked/Operations/OfScientific.olean
+lib/lean/Init/Data/Float/Model/Unpacked/Operations/OfScientific.olean.private
+lib/lean/Init/Data/Float/Model/Unpacked/Operations/OfScientific.olean.server
+lib/lean/Init/Data/Float/Model/Unpacked/Operations/Sign.ilean
+lib/lean/Init/Data/Float/Model/Unpacked/Operations/Sign.ir
+lib/lean/Init/Data/Float/Model/Unpacked/Operations/Sign.ir.sig
+lib/lean/Init/Data/Float/Model/Unpacked/Operations/Sign.olean
+lib/lean/Init/Data/Float/Model/Unpacked/Operations/Sign.olean.private
+lib/lean/Init/Data/Float/Model/Unpacked/Operations/Sign.olean.server
+lib/lean/Init/Data/Float/Model/Unpacked/Operations/Sqrt.ilean
+lib/lean/Init/Data/Float/Model/Unpacked/Operations/Sqrt.ir
+lib/lean/Init/Data/Float/Model/Unpacked/Operations/Sqrt.ir.sig
+lib/lean/Init/Data/Float/Model/Unpacked/Operations/Sqrt.olean
+lib/lean/Init/Data/Float/Model/Unpacked/Operations/Sqrt.olean.private
+lib/lean/Init/Data/Float/Model/Unpacked/Operations/Sqrt.olean.server
+lib/lean/Init/Data/Float/Model/Unpacked/Operations/Status.ilean
+lib/lean/Init/Data/Float/Model/Unpacked/Operations/Status.ir
+lib/lean/Init/Data/Float/Model/Unpacked/Operations/Status.ir.sig
+lib/lean/Init/Data/Float/Model/Unpacked/Operations/Status.olean
+lib/lean/Init/Data/Float/Model/Unpacked/Operations/Status.olean.private
+lib/lean/Init/Data/Float/Model/Unpacked/Operations/Status.olean.server
+lib/lean/Init/Data/Float/Model/Unpacked/Operations/Sub.ilean
+lib/lean/Init/Data/Float/Model/Unpacked/Operations/Sub.ir
+lib/lean/Init/Data/Float/Model/Unpacked/Operations/Sub.ir.sig
+lib/lean/Init/Data/Float/Model/Unpacked/Operations/Sub.olean
+lib/lean/Init/Data/Float/Model/Unpacked/Operations/Sub.olean.private
+lib/lean/Init/Data/Float/Model/Unpacked/Operations/Sub.olean.server
+lib/lean/Init/Data/Float/Model/Unpacked/Operations/ToNat.ilean
+lib/lean/Init/Data/Float/Model/Unpacked/Operations/ToNat.ir
+lib/lean/Init/Data/Float/Model/Unpacked/Operations/ToNat.ir.sig
+lib/lean/Init/Data/Float/Model/Unpacked/Operations/ToNat.olean
+lib/lean/Init/Data/Float/Model/Unpacked/Operations/ToNat.olean.private
+lib/lean/Init/Data/Float/Model/Unpacked/Operations/ToNat.olean.server
*** 14366 LINES SKIPPED ***