From nobody Tue Dec 02 00:47:10 2025 X-Original-To: dev-commits-ports-all@mlmmj.nyi.freebsd.org Received: from mx1.freebsd.org (mx1.freebsd.org [IPv6:2610:1c1:1:606c::19:1]) by mlmmj.nyi.freebsd.org (Postfix) with ESMTP id 4dL2Cz1vH1z6J6Q2 for ; Tue, 02 Dec 2025 00:47:11 +0000 (UTC) (envelope-from git@FreeBSD.org) Received: from mxrelay.nyi.freebsd.org (mxrelay.nyi.freebsd.org [IPv6:2610:1c1:1:606c::19:3]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange X25519 server-signature RSA-PSS (4096 bits) server-digest SHA256 client-signature RSA-PSS (4096 bits) client-digest SHA256) (Client CN "mxrelay.nyi.freebsd.org", Issuer "R12" (verified OK)) by mx1.freebsd.org (Postfix) with ESMTPS id 4dL2Cz1Qx5z3hgl for ; Tue, 02 Dec 2025 00:47:11 +0000 (UTC) (envelope-from git@FreeBSD.org) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=freebsd.org; s=dkim; t=1764636431; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:mime-version:mime-version:content-type:content-type: content-transfer-encoding:content-transfer-encoding; bh=LW8AwlWDgNJTYXv3ezC4zFnSgN3u57rgpjzKpIbuvlo=; b=ohnX0UPc+FOLiq52/Fu5/JZn2xYGIwaWpJQPIHXYGLlxk7MhRRwtjJJJImHXYCH5WH6RKe +i4WdqVm2EtGLm9iX1MWixGDO4d+fSNdrU/+jd619cDds6APEJrU/CbNn2YRyjhRU7z62R 06gTjP11wRGQxK1LqIvnikpfazL+yUBg46yIix726LIleODHjy4H89TdFlWndu0QiVc2lK xSD1ihIxtYRZ3k5z/ZAly9uTbKB9Fyows7pjrGV1IoWLFLu0EOUgRQV6bU1tfVcYtFQ9u0 1sNinbv2DBAFr4OQ9xKByRvWKpSMab94VlI05BBRINRH3uL/sfvVXINfdvuKyA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=freebsd.org; s=dkim; t=1764636431; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:mime-version:mime-version:content-type:content-type: content-transfer-encoding:content-transfer-encoding; bh=LW8AwlWDgNJTYXv3ezC4zFnSgN3u57rgpjzKpIbuvlo=; b=Myh3Qnk81A2MTBXSkAgOw0xFAbsC3+iU64rCxcsVqWfcHiteOPeyxu5tTFmWdDzD7+GIuE 4VKP0rTauaSAsKydzzGF5hqbgvPjjCoa3Nb4hjfpupkd5thdWVOMont95d5O2RQORxL3Be 9t+84Et+A3q4vFcYlmn/UkGMYpen0mbcEHXHoO3fIw21jVBgUaZ3d7A0hjMLCewSPNebia gxwhzX/q0lSFHWtcC3Yf7FHWNbU5NZrzbZ7besAICPayanOb7RYaRUsSegNSCqaxg0g/L+ LLl1fcq2Qfq/KlEMaX81WxhBg0nogJl/StnD6haaq5WJzXbR91fd0gCy4n2nAA== ARC-Seal: i=1; s=dkim; d=freebsd.org; t=1764636431; a=rsa-sha256; cv=none; b=e7QqkMgUlr3EneokAQgYyIyJn5+FRtoX03A4szFIBzvTEo9LFNzubzIZuD4bP/of28ArD0 JUp7kZ/aEeuqDP+svttNvtTEaj74G4f36SIYumBfgbJw292ba/IHf0ORQIZ7TMcc4QDAWg q4BYeFyAni3ppIhTudyi2H2ALBJSge6/VjfsZTjaIxQH5rCE9Se+/gssT/ut6i2CQYF7Y4 O75gtkB0qr3hH4xlHSrcnfBxi/ubsHVyuiEAyZ77+WJoKk1VLw2l/ZujlN9RHMLuAc/tWD eCPVrc1W8v6XJGhKEQU82hPavx1YYncPIq7fdDl9S0L9YID21DfA9mnENBFkFQ== ARC-Authentication-Results: i=1; mx1.freebsd.org; none Received: from gitrepo.freebsd.org (gitrepo.freebsd.org [IPv6:2610:1c1:1:6068::e6a:5]) by mxrelay.nyi.freebsd.org (Postfix) with ESMTP id 4dL2Cz0FnnzlBw for ; Tue, 02 Dec 2025 00:47:11 +0000 (UTC) (envelope-from git@FreeBSD.org) Received: from git (uid 1279) (envelope-from git@FreeBSD.org) id 21c8e by gitrepo.freebsd.org (DragonFly Mail Agent v0.13+ on gitrepo.freebsd.org); Tue, 02 Dec 2025 00:47:10 +0000 To: ports-committers@FreeBSD.org, dev-commits-ports-all@FreeBSD.org, dev-commits-ports-main@FreeBSD.org From: Yuri Victorovich Subject: git: 4d5291902c3a - main - math/lean4: update 4.25.2=?utf-8?Q? =E2=86=92 4.2?=5.2.20251201 List-Id: Commit messages for all branches of the ports repository List-Archive: https://lists.freebsd.org/archives/dev-commits-ports-all List-Help: List-Post: List-Subscribe: List-Unsubscribe: X-BeenThere: dev-commits-ports-all@freebsd.org Sender: owner-dev-commits-ports-all@FreeBSD.org MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: 8bit X-Git-Committer: yuri X-Git-Repository: ports X-Git-Refname: refs/heads/main X-Git-Reftype: branch X-Git-Commit: 4d5291902c3a66649a78ec44d373a6f811b9aa6b Auto-Submitted: auto-generated Date: Tue, 02 Dec 2025 00:47:10 +0000 Message-Id: <692e370e.21c8e.4e99a062@gitrepo.freebsd.org> The branch main has been updated by yuri: URL: https://cgit.FreeBSD.org/ports/commit/?id=4d5291902c3a66649a78ec44d373a6f811b9aa6b commit 4d5291902c3a66649a78ec44d373a6f811b9aa6b Author: Yuri Victorovich AuthorDate: 2025-12-02 00:45:20 +0000 Commit: Yuri Victorovich CommitDate: 2025-12-02 00:47:08 +0000 math/lean4: update 4.25.2 → 4.25.2.20251201 The previous release's tarball changed unexplainably, and the new one is unbuildable, again unexplainably. This update brings it to the latest revision to solve this problem. Reported by: fallout --- math/lean4/Makefile | 5 +- math/lean4/distinfo | 6 +- math/lean4/files/patch-src_shell_CMakeLists.txt | 11 - .../files/patch-stage0_src_shell_CMakeLists.txt | 11 - math/lean4/pkg-plist | 678 +++++++++++++++++---- 5 files changed, 564 insertions(+), 147 deletions(-) diff --git a/math/lean4/Makefile b/math/lean4/Makefile index 30652dafea6b..8b5c81aa12bc 100644 --- a/math/lean4/Makefile +++ b/math/lean4/Makefile @@ -1,6 +1,6 @@ PORTNAME= lean4 DISTVERSIONPREFIX= v -DISTVERSION= 4.25.2 +DISTVERSION= 4.25.2-20251201 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,7 @@ 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 @@ -77,6 +78,6 @@ post-install: lib/lean/libleanshared_1.so \ lib/lean/libLake_shared.so -# tests as of 4.25.2: 100% tests passed, 0 tests failed out of 3241 +# tests as of 4.25.2-20251201: 100% tests passed, 0 tests failed out of 3367 .include diff --git a/math/lean4/distinfo b/math/lean4/distinfo index ca359438cd41..20923ac21be3 100644 --- a/math/lean4/distinfo +++ b/math/lean4/distinfo @@ -1,3 +1,3 @@ -TIMESTAMP = 1764048066 -SHA256 (leanprover-lean4-v4.25.2_GH0.tar.gz) = 831b1d1d3833791e68de087d8f576c4703a5dd82157dd19364629f5df7fcfb2c -SIZE (leanprover-lean4-v4.25.2_GH0.tar.gz) = 50069767 +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 diff --git a/math/lean4/files/patch-src_shell_CMakeLists.txt b/math/lean4/files/patch-src_shell_CMakeLists.txt deleted file mode 100644 index 68de472208ff..000000000000 --- a/math/lean4/files/patch-src_shell_CMakeLists.txt +++ /dev/null @@ -1,11 +0,0 @@ ---- src/shell/CMakeLists.txt.orig 2025-11-18 02:29:21 UTC -+++ src/shell/CMakeLists.txt -@@ -57,7 +57,7 @@ endif() - endif() - - # LEANC_OPTS in CXX is necessary for macOS c++ to find its headers --set(TEST_VARS "PATH=${LEAN_BIN}:$PATH ${LEAN_TEST_VARS} CXX='${CMAKE_CXX_COMPILER} ${LEANC_OPTS}' LEANC_OPTS='${LEANC_OPTS}'") -+set(TEST_VARS "PATH=${LEAN_BIN}:$PATH LD_LIBRARY_PATH=${CMAKE_BINARY_DIR}/lib/lean:\${LD_LIBRARY_PATH:-} ${LEAN_TEST_VARS} CXX='${CMAKE_CXX_COMPILER} ${LEANC_OPTS}' LEANC_OPTS='${LEANC_OPTS}'") - - # LEAN TESTS - file(GLOB LEANTESTS "${LEAN_SOURCE_DIR}/../tests/lean/*.lean") diff --git a/math/lean4/files/patch-stage0_src_shell_CMakeLists.txt b/math/lean4/files/patch-stage0_src_shell_CMakeLists.txt deleted file mode 100644 index bd9010ce3d9b..000000000000 --- a/math/lean4/files/patch-stage0_src_shell_CMakeLists.txt +++ /dev/null @@ -1,11 +0,0 @@ ---- stage0/src/shell/CMakeLists.txt.orig 2025-11-18 02:29:21 UTC -+++ stage0/src/shell/CMakeLists.txt -@@ -57,7 +57,7 @@ endif() - endif() - - # LEANC_OPTS in CXX is necessary for macOS c++ to find its headers --set(TEST_VARS "PATH=${LEAN_BIN}:$PATH ${LEAN_TEST_VARS} CXX='${CMAKE_CXX_COMPILER} ${LEANC_OPTS}' LEANC_OPTS='${LEANC_OPTS}'") -+set(TEST_VARS "PATH=${LEAN_BIN}:$PATH LD_LIBRARY_PATH=${CMAKE_BINARY_DIR}/lib/lean:\${LD_LIBRARY_PATH:-} ${LEAN_TEST_VARS} CXX='${CMAKE_CXX_COMPILER} ${LEANC_OPTS}' LEANC_OPTS='${LEANC_OPTS}'") - - # LEAN TESTS - file(GLOB LEANTESTS "${LEAN_SOURCE_DIR}/../tests/lean/*.lean") diff --git a/math/lean4/pkg-plist b/math/lean4/pkg-plist index b35afb3ef8ff..ae09be366a40 100644 --- a/math/lean4/pkg-plist +++ b/math/lean4/pkg-plist @@ -317,11 +317,6 @@ 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/Basic.ilean -lib/lean/Init/Data/Basic.ir -lib/lean/Init/Data/Basic.olean -lib/lean/Init/Data/Basic.olean.private -lib/lean/Init/Data/Basic.olean.server lib/lean/Init/Data/BitVec.ilean lib/lean/Init/Data/BitVec.ir lib/lean/Init/Data/BitVec.olean @@ -587,6 +582,11 @@ 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 @@ -672,11 +672,21 @@ lib/lean/Init/Data/Iterators/Combinators/Monadic/FlatMap.ir lib/lean/Init/Data/Iterators/Combinators/Monadic/FlatMap.olean lib/lean/Init/Data/Iterators/Combinators/Monadic/FlatMap.olean.private lib/lean/Init/Data/Iterators/Combinators/Monadic/FlatMap.olean.server +lib/lean/Init/Data/Iterators/Combinators/Monadic/Take.ilean +lib/lean/Init/Data/Iterators/Combinators/Monadic/Take.ir +lib/lean/Init/Data/Iterators/Combinators/Monadic/Take.olean +lib/lean/Init/Data/Iterators/Combinators/Monadic/Take.olean.private +lib/lean/Init/Data/Iterators/Combinators/Monadic/Take.olean.server lib/lean/Init/Data/Iterators/Combinators/Monadic/ULift.ilean lib/lean/Init/Data/Iterators/Combinators/Monadic/ULift.ir lib/lean/Init/Data/Iterators/Combinators/Monadic/ULift.olean lib/lean/Init/Data/Iterators/Combinators/Monadic/ULift.olean.private lib/lean/Init/Data/Iterators/Combinators/Monadic/ULift.olean.server +lib/lean/Init/Data/Iterators/Combinators/Take.ilean +lib/lean/Init/Data/Iterators/Combinators/Take.ir +lib/lean/Init/Data/Iterators/Combinators/Take.olean +lib/lean/Init/Data/Iterators/Combinators/Take.olean.private +lib/lean/Init/Data/Iterators/Combinators/Take.olean.server lib/lean/Init/Data/Iterators/Combinators/ULift.ilean lib/lean/Init/Data/Iterators/Combinators/ULift.ir lib/lean/Init/Data/Iterators/Combinators/ULift.olean @@ -802,11 +812,21 @@ lib/lean/Init/Data/Iterators/Lemmas/Combinators/Monadic/FlatMap.ir lib/lean/Init/Data/Iterators/Lemmas/Combinators/Monadic/FlatMap.olean lib/lean/Init/Data/Iterators/Lemmas/Combinators/Monadic/FlatMap.olean.private lib/lean/Init/Data/Iterators/Lemmas/Combinators/Monadic/FlatMap.olean.server +lib/lean/Init/Data/Iterators/Lemmas/Combinators/Monadic/Take.ilean +lib/lean/Init/Data/Iterators/Lemmas/Combinators/Monadic/Take.ir +lib/lean/Init/Data/Iterators/Lemmas/Combinators/Monadic/Take.olean +lib/lean/Init/Data/Iterators/Lemmas/Combinators/Monadic/Take.olean.private +lib/lean/Init/Data/Iterators/Lemmas/Combinators/Monadic/Take.olean.server lib/lean/Init/Data/Iterators/Lemmas/Combinators/Monadic/ULift.ilean lib/lean/Init/Data/Iterators/Lemmas/Combinators/Monadic/ULift.ir lib/lean/Init/Data/Iterators/Lemmas/Combinators/Monadic/ULift.olean lib/lean/Init/Data/Iterators/Lemmas/Combinators/Monadic/ULift.olean.private lib/lean/Init/Data/Iterators/Lemmas/Combinators/Monadic/ULift.olean.server +lib/lean/Init/Data/Iterators/Lemmas/Combinators/Take.ilean +lib/lean/Init/Data/Iterators/Lemmas/Combinators/Take.ir +lib/lean/Init/Data/Iterators/Lemmas/Combinators/Take.olean +lib/lean/Init/Data/Iterators/Lemmas/Combinators/Take.olean.private +lib/lean/Init/Data/Iterators/Lemmas/Combinators/Take.olean.server lib/lean/Init/Data/Iterators/Lemmas/Combinators/ULift.ilean lib/lean/Init/Data/Iterators/Lemmas/Combinators/ULift.ir lib/lean/Init/Data/Iterators/Lemmas/Combinators/ULift.olean @@ -847,11 +867,51 @@ lib/lean/Init/Data/Iterators/Lemmas/Monadic/Basic.ir lib/lean/Init/Data/Iterators/Lemmas/Monadic/Basic.olean lib/lean/Init/Data/Iterators/Lemmas/Monadic/Basic.olean.private lib/lean/Init/Data/Iterators/Lemmas/Monadic/Basic.olean.server +lib/lean/Init/Data/Iterators/Lemmas/Producers.ilean +lib/lean/Init/Data/Iterators/Lemmas/Producers.ir +lib/lean/Init/Data/Iterators/Lemmas/Producers.olean +lib/lean/Init/Data/Iterators/Lemmas/Producers.olean.private +lib/lean/Init/Data/Iterators/Lemmas/Producers.olean.server +lib/lean/Init/Data/Iterators/Lemmas/Producers/List.ilean +lib/lean/Init/Data/Iterators/Lemmas/Producers/List.ir +lib/lean/Init/Data/Iterators/Lemmas/Producers/List.olean +lib/lean/Init/Data/Iterators/Lemmas/Producers/List.olean.private +lib/lean/Init/Data/Iterators/Lemmas/Producers/List.olean.server +lib/lean/Init/Data/Iterators/Lemmas/Producers/Monadic.ilean +lib/lean/Init/Data/Iterators/Lemmas/Producers/Monadic.ir +lib/lean/Init/Data/Iterators/Lemmas/Producers/Monadic.olean +lib/lean/Init/Data/Iterators/Lemmas/Producers/Monadic.olean.private +lib/lean/Init/Data/Iterators/Lemmas/Producers/Monadic.olean.server +lib/lean/Init/Data/Iterators/Lemmas/Producers/Monadic/List.ilean +lib/lean/Init/Data/Iterators/Lemmas/Producers/Monadic/List.ir +lib/lean/Init/Data/Iterators/Lemmas/Producers/Monadic/List.olean +lib/lean/Init/Data/Iterators/Lemmas/Producers/Monadic/List.olean.private +lib/lean/Init/Data/Iterators/Lemmas/Producers/Monadic/List.olean.server lib/lean/Init/Data/Iterators/PostconditionMonad.ilean lib/lean/Init/Data/Iterators/PostconditionMonad.ir lib/lean/Init/Data/Iterators/PostconditionMonad.olean lib/lean/Init/Data/Iterators/PostconditionMonad.olean.private lib/lean/Init/Data/Iterators/PostconditionMonad.olean.server +lib/lean/Init/Data/Iterators/Producers.ilean +lib/lean/Init/Data/Iterators/Producers.ir +lib/lean/Init/Data/Iterators/Producers.olean +lib/lean/Init/Data/Iterators/Producers.olean.private +lib/lean/Init/Data/Iterators/Producers.olean.server +lib/lean/Init/Data/Iterators/Producers/List.ilean +lib/lean/Init/Data/Iterators/Producers/List.ir +lib/lean/Init/Data/Iterators/Producers/List.olean +lib/lean/Init/Data/Iterators/Producers/List.olean.private +lib/lean/Init/Data/Iterators/Producers/List.olean.server +lib/lean/Init/Data/Iterators/Producers/Monadic.ilean +lib/lean/Init/Data/Iterators/Producers/Monadic.ir +lib/lean/Init/Data/Iterators/Producers/Monadic.olean +lib/lean/Init/Data/Iterators/Producers/Monadic.olean.private +lib/lean/Init/Data/Iterators/Producers/Monadic.olean.server +lib/lean/Init/Data/Iterators/Producers/Monadic/List.ilean +lib/lean/Init/Data/Iterators/Producers/Monadic/List.ir +lib/lean/Init/Data/Iterators/Producers/Monadic/List.olean +lib/lean/Init/Data/Iterators/Producers/Monadic/List.olean.private +lib/lean/Init/Data/Iterators/Producers/Monadic/List.olean.server lib/lean/Init/Data/Iterators/ToIterator.ilean lib/lean/Init/Data/Iterators/ToIterator.ir lib/lean/Init/Data/Iterators/ToIterator.olean @@ -1407,6 +1467,11 @@ lib/lean/Init/Data/Range/Polymorphic/Int.ir lib/lean/Init/Data/Range/Polymorphic/Int.olean lib/lean/Init/Data/Range/Polymorphic/Int.olean.private lib/lean/Init/Data/Range/Polymorphic/Int.olean.server +lib/lean/Init/Data/Range/Polymorphic/IntLemmas.ilean +lib/lean/Init/Data/Range/Polymorphic/IntLemmas.ir +lib/lean/Init/Data/Range/Polymorphic/IntLemmas.olean +lib/lean/Init/Data/Range/Polymorphic/IntLemmas.olean.private +lib/lean/Init/Data/Range/Polymorphic/IntLemmas.olean.server lib/lean/Init/Data/Range/Polymorphic/Internal/SignedBitVec.ilean lib/lean/Init/Data/Range/Polymorphic/Internal/SignedBitVec.ir lib/lean/Init/Data/Range/Polymorphic/Internal/SignedBitVec.olean @@ -1547,6 +1612,26 @@ lib/lean/Init/Data/Slice/Lemmas.ir lib/lean/Init/Data/Slice/Lemmas.olean lib/lean/Init/Data/Slice/Lemmas.olean.private lib/lean/Init/Data/Slice/Lemmas.olean.server +lib/lean/Init/Data/Slice/List.ilean +lib/lean/Init/Data/Slice/List.ir +lib/lean/Init/Data/Slice/List.olean +lib/lean/Init/Data/Slice/List.olean.private +lib/lean/Init/Data/Slice/List.olean.server +lib/lean/Init/Data/Slice/List/Basic.ilean +lib/lean/Init/Data/Slice/List/Basic.ir +lib/lean/Init/Data/Slice/List/Basic.olean +lib/lean/Init/Data/Slice/List/Basic.olean.private +lib/lean/Init/Data/Slice/List/Basic.olean.server +lib/lean/Init/Data/Slice/List/Iterator.ilean +lib/lean/Init/Data/Slice/List/Iterator.ir +lib/lean/Init/Data/Slice/List/Iterator.olean +lib/lean/Init/Data/Slice/List/Iterator.olean.private +lib/lean/Init/Data/Slice/List/Iterator.olean.server +lib/lean/Init/Data/Slice/List/Lemmas.ilean +lib/lean/Init/Data/Slice/List/Lemmas.ir +lib/lean/Init/Data/Slice/List/Lemmas.olean +lib/lean/Init/Data/Slice/List/Lemmas.olean.private +lib/lean/Init/Data/Slice/List/Lemmas.olean.server lib/lean/Init/Data/Slice/Notation.ilean lib/lean/Init/Data/Slice/Notation.ir lib/lean/Init/Data/Slice/Notation.olean @@ -1582,16 +1667,61 @@ lib/lean/Init/Data/String/Decode.ir lib/lean/Init/Data/String/Decode.olean lib/lean/Init/Data/String/Decode.olean.private lib/lean/Init/Data/String/Decode.olean.server +lib/lean/Init/Data/String/Defs.ilean +lib/lean/Init/Data/String/Defs.ir +lib/lean/Init/Data/String/Defs.olean +lib/lean/Init/Data/String/Defs.olean.private +lib/lean/Init/Data/String/Defs.olean.server lib/lean/Init/Data/String/Extra.ilean 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/Iterator.ilean +lib/lean/Init/Data/String/Iterator.ir +lib/lean/Init/Data/String/Iterator.olean +lib/lean/Init/Data/String/Iterator.olean.private +lib/lean/Init/Data/String/Iterator.olean.server +lib/lean/Init/Data/String/Legacy.ilean +lib/lean/Init/Data/String/Legacy.ir +lib/lean/Init/Data/String/Legacy.olean +lib/lean/Init/Data/String/Legacy.olean.private +lib/lean/Init/Data/String/Legacy.olean.server lib/lean/Init/Data/String/Lemmas.ilean lib/lean/Init/Data/String/Lemmas.ir lib/lean/Init/Data/String/Lemmas.olean lib/lean/Init/Data/String/Lemmas.olean.private lib/lean/Init/Data/String/Lemmas.olean.server +lib/lean/Init/Data/String/Lemmas/Basic.ilean +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/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/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/Splits.ilean +lib/lean/Init/Data/String/Lemmas/Splits.ir +lib/lean/Init/Data/String/Lemmas/Splits.olean +lib/lean/Init/Data/String/Lemmas/Splits.olean.private +lib/lean/Init/Data/String/Lemmas/Splits.olean.server +lib/lean/Init/Data/String/Modify.ilean +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/Pattern.ilean lib/lean/Init/Data/String/Pattern.ir lib/lean/Init/Data/String/Pattern.olean @@ -1617,11 +1747,16 @@ lib/lean/Init/Data/String/Pattern/String.ir lib/lean/Init/Data/String/Pattern/String.olean lib/lean/Init/Data/String/Pattern/String.olean.private lib/lean/Init/Data/String/Pattern/String.olean.server -lib/lean/Init/Data/String/Repr.ilean -lib/lean/Init/Data/String/Repr.ir -lib/lean/Init/Data/String/Repr.olean -lib/lean/Init/Data/String/Repr.olean.private -lib/lean/Init/Data/String/Repr.olean.server +lib/lean/Init/Data/String/PosRaw.ilean +lib/lean/Init/Data/String/PosRaw.ir +lib/lean/Init/Data/String/PosRaw.olean +lib/lean/Init/Data/String/PosRaw.olean.private +lib/lean/Init/Data/String/PosRaw.olean.server +lib/lean/Init/Data/String/Search.ilean +lib/lean/Init/Data/String/Search.ir +lib/lean/Init/Data/String/Search.olean +lib/lean/Init/Data/String/Search.olean.private +lib/lean/Init/Data/String/Search.olean.server lib/lean/Init/Data/String/Slice.ilean lib/lean/Init/Data/String/Slice.ir lib/lean/Init/Data/String/Slice.olean @@ -1632,6 +1767,26 @@ 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/Substring.ilean +lib/lean/Init/Data/String/Substring.ir +lib/lean/Init/Data/String/Substring.olean +lib/lean/Init/Data/String/Substring.olean.private +lib/lean/Init/Data/String/Substring.olean.server +lib/lean/Init/Data/String/TakeDrop.ilean +lib/lean/Init/Data/String/TakeDrop.ir +lib/lean/Init/Data/String/TakeDrop.olean +lib/lean/Init/Data/String/TakeDrop.olean.private +lib/lean/Init/Data/String/TakeDrop.olean.server +lib/lean/Init/Data/String/Termination.ilean +lib/lean/Init/Data/String/Termination.ir +lib/lean/Init/Data/String/Termination.olean +lib/lean/Init/Data/String/Termination.olean.private +lib/lean/Init/Data/String/Termination.olean.server +lib/lean/Init/Data/String/ToSlice.ilean +lib/lean/Init/Data/String/ToSlice.ir +lib/lean/Init/Data/String/ToSlice.olean +lib/lean/Init/Data/String/ToSlice.olean.private +lib/lean/Init/Data/String/ToSlice.olean.server lib/lean/Init/Data/Subtype.ilean lib/lean/Init/Data/Subtype.ir lib/lean/Init/Data/Subtype.olean @@ -1852,6 +2007,11 @@ lib/lean/Init/Grind/AC.ir lib/lean/Init/Grind/AC.olean lib/lean/Init/Grind/AC.olean.private lib/lean/Init/Grind/AC.olean.server +lib/lean/Init/Grind/Annotated.ilean +lib/lean/Init/Grind/Annotated.ir +lib/lean/Init/Grind/Annotated.olean +lib/lean/Init/Grind/Annotated.olean.private +lib/lean/Init/Grind/Annotated.olean.server lib/lean/Init/Grind/Attr.ilean lib/lean/Init/Grind/Attr.ir lib/lean/Init/Grind/Attr.olean @@ -1862,11 +2022,21 @@ lib/lean/Init/Grind/Cases.ir lib/lean/Init/Grind/Cases.olean lib/lean/Init/Grind/Cases.olean.private lib/lean/Init/Grind/Cases.olean.server +lib/lean/Init/Grind/Config.ilean +lib/lean/Init/Grind/Config.ir +lib/lean/Init/Grind/Config.olean +lib/lean/Init/Grind/Config.olean.private +lib/lean/Init/Grind/Config.olean.server lib/lean/Init/Grind/Ext.ilean lib/lean/Init/Grind/Ext.ir lib/lean/Init/Grind/Ext.olean lib/lean/Init/Grind/Ext.olean.private lib/lean/Init/Grind/Ext.olean.server +lib/lean/Init/Grind/FieldNormNum.ilean +lib/lean/Init/Grind/FieldNormNum.ir +lib/lean/Init/Grind/FieldNormNum.olean +lib/lean/Init/Grind/FieldNormNum.olean.private +lib/lean/Init/Grind/FieldNormNum.olean.server lib/lean/Init/Grind/Injective.ilean lib/lean/Init/Grind/Injective.ir lib/lean/Init/Grind/Injective.olean @@ -1882,6 +2052,11 @@ lib/lean/Init/Grind/Lemmas.ir lib/lean/Init/Grind/Lemmas.olean lib/lean/Init/Grind/Lemmas.olean.private lib/lean/Init/Grind/Lemmas.olean.server +lib/lean/Init/Grind/Lint.ilean +lib/lean/Init/Grind/Lint.ir +lib/lean/Init/Grind/Lint.olean +lib/lean/Init/Grind/Lint.olean.private +lib/lean/Init/Grind/Lint.olean.server lib/lean/Init/Grind/Module.ilean lib/lean/Init/Grind/Module.ir lib/lean/Init/Grind/Module.olean @@ -2002,6 +2177,11 @@ lib/lean/Init/Grind/Ring/Field.ir lib/lean/Init/Grind/Ring/Field.olean lib/lean/Init/Grind/Ring/Field.olean.private lib/lean/Init/Grind/Ring/Field.olean.server +lib/lean/Init/Grind/Ring/OfScientific.ilean +lib/lean/Init/Grind/Ring/OfScientific.ir +lib/lean/Init/Grind/Ring/OfScientific.olean +lib/lean/Init/Grind/Ring/OfScientific.olean.private +lib/lean/Init/Grind/Ring/OfScientific.olean.server lib/lean/Init/Grind/Ring/ToInt.ilean lib/lean/Init/Grind/Ring/ToInt.ir lib/lean/Init/Grind/Ring/ToInt.olean @@ -3292,6 +3472,11 @@ 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 @@ -3422,6 +3607,11 @@ lib/lean/Lean/Compiler/LCNF/Internalize.ir lib/lean/Lean/Compiler/LCNF/Internalize.olean lib/lean/Lean/Compiler/LCNF/Internalize.olean.private lib/lean/Lean/Compiler/LCNF/Internalize.olean.server +lib/lean/Lean/Compiler/LCNF/Irrelevant.ilean +lib/lean/Lean/Compiler/LCNF/Irrelevant.ir +lib/lean/Lean/Compiler/LCNF/Irrelevant.olean +lib/lean/Lean/Compiler/LCNF/Irrelevant.olean.private +lib/lean/Lean/Compiler/LCNF/Irrelevant.olean.server lib/lean/Lean/Compiler/LCNF/JoinPoints.ilean lib/lean/Lean/Compiler/LCNF/JoinPoints.ir lib/lean/Lean/Compiler/LCNF/JoinPoints.olean @@ -3652,6 +3842,11 @@ lib/lean/Lean/Compiler/MetaAttr.ir lib/lean/Lean/Compiler/MetaAttr.olean lib/lean/Lean/Compiler/MetaAttr.olean.private lib/lean/Lean/Compiler/MetaAttr.olean.server +lib/lean/Lean/Compiler/ModPkgExt.ilean +lib/lean/Lean/Compiler/ModPkgExt.ir +lib/lean/Lean/Compiler/ModPkgExt.olean +lib/lean/Lean/Compiler/ModPkgExt.olean.private +lib/lean/Lean/Compiler/ModPkgExt.olean.server lib/lean/Lean/Compiler/NameMangling.ilean lib/lean/Lean/Compiler/NameMangling.ir lib/lean/Lean/Compiler/NameMangling.olean @@ -4132,6 +4327,11 @@ lib/lean/Lean/Elab/Command/Scope.ir lib/lean/Lean/Elab/Command/Scope.olean lib/lean/Lean/Elab/Command/Scope.olean.private lib/lean/Lean/Elab/Command/Scope.olean.server +lib/lean/Lean/Elab/Command/WithWeakNamespace.ilean +lib/lean/Lean/Elab/Command/WithWeakNamespace.ir +lib/lean/Lean/Elab/Command/WithWeakNamespace.olean +lib/lean/Lean/Elab/Command/WithWeakNamespace.olean.private +lib/lean/Lean/Elab/Command/WithWeakNamespace.olean.server lib/lean/Lean/Elab/ComputedFields.ilean lib/lean/Lean/Elab/ComputedFields.ir lib/lean/Lean/Elab/ComputedFields.olean @@ -4257,6 +4457,21 @@ lib/lean/Lean/Elab/Do.ir lib/lean/Lean/Elab/Do.olean lib/lean/Lean/Elab/Do.olean.private lib/lean/Lean/Elab/Do.olean.server +lib/lean/Lean/Elab/Do/Basic.ilean +lib/lean/Lean/Elab/Do/Basic.ir +lib/lean/Lean/Elab/Do/Basic.olean +lib/lean/Lean/Elab/Do/Basic.olean.private +lib/lean/Lean/Elab/Do/Basic.olean.server +lib/lean/Lean/Elab/Do/Legacy.ilean +lib/lean/Lean/Elab/Do/Legacy.ir +lib/lean/Lean/Elab/Do/Legacy.olean +lib/lean/Lean/Elab/Do/Legacy.olean.private +lib/lean/Lean/Elab/Do/Legacy.olean.server +lib/lean/Lean/Elab/Do/Switch.ilean +lib/lean/Lean/Elab/Do/Switch.ir +lib/lean/Lean/Elab/Do/Switch.olean +lib/lean/Lean/Elab/Do/Switch.olean.private +lib/lean/Lean/Elab/Do/Switch.olean.server lib/lean/Lean/Elab/DocString.ilean lib/lean/Lean/Elab/DocString.ir lib/lean/Lean/Elab/DocString.olean @@ -4432,6 +4647,11 @@ lib/lean/Lean/Elab/Open.ir lib/lean/Lean/Elab/Open.olean lib/lean/Lean/Elab/Open.olean.private lib/lean/Lean/Elab/Open.olean.server +lib/lean/Lean/Elab/Parallel.ilean +lib/lean/Lean/Elab/Parallel.ir +lib/lean/Lean/Elab/Parallel.olean +lib/lean/Lean/Elab/Parallel.olean.private +lib/lean/Lean/Elab/Parallel.olean.server lib/lean/Lean/Elab/ParseImportsFast.ilean lib/lean/Lean/Elab/ParseImportsFast.ir lib/lean/Lean/Elab/ParseImportsFast.olean @@ -4882,6 +5102,11 @@ lib/lean/Lean/Elab/Tactic/Config.ir lib/lean/Lean/Elab/Tactic/Config.olean lib/lean/Lean/Elab/Tactic/Config.olean.private lib/lean/Lean/Elab/Tactic/Config.olean.server +lib/lean/Lean/Elab/Tactic/ConfigSetter.ilean +lib/lean/Lean/Elab/Tactic/ConfigSetter.ir +lib/lean/Lean/Elab/Tactic/ConfigSetter.olean +lib/lean/Lean/Elab/Tactic/ConfigSetter.olean.private +lib/lean/Lean/Elab/Tactic/ConfigSetter.olean.server lib/lean/Lean/Elab/Tactic/Congr.ilean lib/lean/Lean/Elab/Tactic/Congr.ir lib/lean/Lean/Elab/Tactic/Congr.olean @@ -5127,6 +5352,16 @@ lib/lean/Lean/Elab/Tactic/Grind.ir lib/lean/Lean/Elab/Tactic/Grind.olean lib/lean/Lean/Elab/Tactic/Grind.olean.private lib/lean/Lean/Elab/Tactic/Grind.olean.server +lib/lean/Lean/Elab/Tactic/Grind/Anchor.ilean +lib/lean/Lean/Elab/Tactic/Grind/Anchor.ir +lib/lean/Lean/Elab/Tactic/Grind/Anchor.olean +lib/lean/Lean/Elab/Tactic/Grind/Anchor.olean.private +lib/lean/Lean/Elab/Tactic/Grind/Anchor.olean.server +lib/lean/Lean/Elab/Tactic/Grind/Annotated.ilean +lib/lean/Lean/Elab/Tactic/Grind/Annotated.ir +lib/lean/Lean/Elab/Tactic/Grind/Annotated.olean +lib/lean/Lean/Elab/Tactic/Grind/Annotated.olean.private +lib/lean/Lean/Elab/Tactic/Grind/Annotated.olean.server lib/lean/Lean/Elab/Tactic/Grind/Basic.ilean lib/lean/Lean/Elab/Tactic/Grind/Basic.ir lib/lean/Lean/Elab/Tactic/Grind/Basic.olean @@ -5137,6 +5372,11 @@ lib/lean/Lean/Elab/Tactic/Grind/BuiltinTactic.ir lib/lean/Lean/Elab/Tactic/Grind/BuiltinTactic.olean lib/lean/Lean/Elab/Tactic/Grind/BuiltinTactic.olean.private lib/lean/Lean/Elab/Tactic/Grind/BuiltinTactic.olean.server +lib/lean/Lean/Elab/Tactic/Grind/Config.ilean +lib/lean/Lean/Elab/Tactic/Grind/Config.ir +lib/lean/Lean/Elab/Tactic/Grind/Config.olean +lib/lean/Lean/Elab/Tactic/Grind/Config.olean.private +lib/lean/Lean/Elab/Tactic/Grind/Config.olean.server lib/lean/Lean/Elab/Tactic/Grind/Filter.ilean lib/lean/Lean/Elab/Tactic/Grind/Filter.ir lib/lean/Lean/Elab/Tactic/Grind/Filter.olean @@ -5147,11 +5387,26 @@ lib/lean/Lean/Elab/Tactic/Grind/Have.ir lib/lean/Lean/Elab/Tactic/Grind/Have.olean lib/lean/Lean/Elab/Tactic/Grind/Have.olean.private lib/lean/Lean/Elab/Tactic/Grind/Have.olean.server +lib/lean/Lean/Elab/Tactic/Grind/Lint.ilean +lib/lean/Lean/Elab/Tactic/Grind/Lint.ir +lib/lean/Lean/Elab/Tactic/Grind/Lint.olean +lib/lean/Lean/Elab/Tactic/Grind/Lint.olean.private +lib/lean/Lean/Elab/Tactic/Grind/Lint.olean.server +lib/lean/Lean/Elab/Tactic/Grind/LintExceptions.ilean +lib/lean/Lean/Elab/Tactic/Grind/LintExceptions.ir +lib/lean/Lean/Elab/Tactic/Grind/LintExceptions.olean +lib/lean/Lean/Elab/Tactic/Grind/LintExceptions.olean.private +lib/lean/Lean/Elab/Tactic/Grind/LintExceptions.olean.server lib/lean/Lean/Elab/Tactic/Grind/Main.ilean lib/lean/Lean/Elab/Tactic/Grind/Main.ir lib/lean/Lean/Elab/Tactic/Grind/Main.olean lib/lean/Lean/Elab/Tactic/Grind/Main.olean.private lib/lean/Lean/Elab/Tactic/Grind/Main.olean.server +lib/lean/Lean/Elab/Tactic/Grind/Param.ilean +lib/lean/Lean/Elab/Tactic/Grind/Param.ir +lib/lean/Lean/Elab/Tactic/Grind/Param.olean +lib/lean/Lean/Elab/Tactic/Grind/Param.olean.private +lib/lean/Lean/Elab/Tactic/Grind/Param.olean.server lib/lean/Lean/Elab/Tactic/Grind/ShowState.ilean lib/lean/Lean/Elab/Tactic/Grind/ShowState.ir lib/lean/Lean/Elab/Tactic/Grind/ShowState.olean @@ -5332,6 +5587,11 @@ lib/lean/Lean/Elab/Tactic/Unfold.ir lib/lean/Lean/Elab/Tactic/Unfold.olean lib/lean/Lean/Elab/Tactic/Unfold.olean.private lib/lean/Lean/Elab/Tactic/Unfold.olean.server +lib/lean/Lean/Elab/Task.ilean +lib/lean/Lean/Elab/Task.ir +lib/lean/Lean/Elab/Task.olean +lib/lean/Lean/Elab/Task.olean.private +lib/lean/Lean/Elab/Task.olean.server lib/lean/Lean/Elab/Term.ilean lib/lean/Lean/Elab/Term.ir lib/lean/Lean/Elab/Term.olean @@ -5387,6 +5647,11 @@ lib/lean/Lean/ErrorExplanations/DependsOnNoncomputable.ir lib/lean/Lean/ErrorExplanations/DependsOnNoncomputable.olean lib/lean/Lean/ErrorExplanations/DependsOnNoncomputable.olean.private lib/lean/Lean/ErrorExplanations/DependsOnNoncomputable.olean.server +lib/lean/Lean/ErrorExplanations/InductionWithNoAlts.ilean +lib/lean/Lean/ErrorExplanations/InductionWithNoAlts.ir +lib/lean/Lean/ErrorExplanations/InductionWithNoAlts.olean +lib/lean/Lean/ErrorExplanations/InductionWithNoAlts.olean.private +lib/lean/Lean/ErrorExplanations/InductionWithNoAlts.olean.server lib/lean/Lean/ErrorExplanations/InductiveParamMismatch.ilean lib/lean/Lean/ErrorExplanations/InductiveParamMismatch.ir lib/lean/Lean/ErrorExplanations/InductiveParamMismatch.olean @@ -5427,6 +5692,11 @@ lib/lean/Lean/ErrorExplanations/RedundantMatchAlt.ir lib/lean/Lean/ErrorExplanations/RedundantMatchAlt.olean lib/lean/Lean/ErrorExplanations/RedundantMatchAlt.olean.private lib/lean/Lean/ErrorExplanations/RedundantMatchAlt.olean.server +lib/lean/Lean/ErrorExplanations/SynthInstanceFailed.ilean +lib/lean/Lean/ErrorExplanations/SynthInstanceFailed.ir +lib/lean/Lean/ErrorExplanations/SynthInstanceFailed.olean +lib/lean/Lean/ErrorExplanations/SynthInstanceFailed.olean.private +lib/lean/Lean/ErrorExplanations/SynthInstanceFailed.olean.server lib/lean/Lean/ErrorExplanations/UnknownIdentifier.ilean lib/lean/Lean/ErrorExplanations/UnknownIdentifier.ir lib/lean/Lean/ErrorExplanations/UnknownIdentifier.olean @@ -5502,6 +5772,36 @@ lib/lean/Lean/Level.ir lib/lean/Lean/Level.olean lib/lean/Lean/Level.olean.private lib/lean/Lean/Level.olean.server +lib/lean/Lean/LibrarySuggestions.ilean +lib/lean/Lean/LibrarySuggestions.ir +lib/lean/Lean/LibrarySuggestions.olean +lib/lean/Lean/LibrarySuggestions.olean.private +lib/lean/Lean/LibrarySuggestions.olean.server +lib/lean/Lean/LibrarySuggestions/Basic.ilean +lib/lean/Lean/LibrarySuggestions/Basic.ir +lib/lean/Lean/LibrarySuggestions/Basic.olean +lib/lean/Lean/LibrarySuggestions/Basic.olean.private +lib/lean/Lean/LibrarySuggestions/Basic.olean.server +lib/lean/Lean/LibrarySuggestions/Default.ilean +lib/lean/Lean/LibrarySuggestions/Default.ir +lib/lean/Lean/LibrarySuggestions/Default.olean +lib/lean/Lean/LibrarySuggestions/Default.olean.private +lib/lean/Lean/LibrarySuggestions/Default.olean.server +lib/lean/Lean/LibrarySuggestions/MePo.ilean +lib/lean/Lean/LibrarySuggestions/MePo.ir +lib/lean/Lean/LibrarySuggestions/MePo.olean +lib/lean/Lean/LibrarySuggestions/MePo.olean.private +lib/lean/Lean/LibrarySuggestions/MePo.olean.server +lib/lean/Lean/LibrarySuggestions/SineQuaNon.ilean +lib/lean/Lean/LibrarySuggestions/SineQuaNon.ir +lib/lean/Lean/LibrarySuggestions/SineQuaNon.olean +lib/lean/Lean/LibrarySuggestions/SineQuaNon.olean.private +lib/lean/Lean/LibrarySuggestions/SineQuaNon.olean.server +lib/lean/Lean/LibrarySuggestions/SymbolFrequency.ilean +lib/lean/Lean/LibrarySuggestions/SymbolFrequency.ir +lib/lean/Lean/LibrarySuggestions/SymbolFrequency.olean +lib/lean/Lean/LibrarySuggestions/SymbolFrequency.olean.private +lib/lean/Lean/LibrarySuggestions/SymbolFrequency.olean.server lib/lean/Lean/Linter.ilean lib/lean/Lean/Linter.ir lib/lean/Lean/Linter.olean @@ -5637,6 +5937,11 @@ lib/lean/Lean/Meta/Canonicalizer.ir lib/lean/Lean/Meta/Canonicalizer.olean lib/lean/Lean/Meta/Canonicalizer.olean.private lib/lean/Lean/Meta/Canonicalizer.olean.server +lib/lean/Lean/Meta/CasesInfo.ilean +lib/lean/Lean/Meta/CasesInfo.ir +lib/lean/Lean/Meta/CasesInfo.olean +lib/lean/Lean/Meta/CasesInfo.olean.private +lib/lean/Lean/Meta/CasesInfo.olean.server lib/lean/Lean/Meta/Check.ilean lib/lean/Lean/Meta/Check.ir lib/lean/Lean/Meta/Check.olean @@ -5722,6 +6027,11 @@ lib/lean/Lean/Meta/Constructions/RecOn.ir lib/lean/Lean/Meta/Constructions/RecOn.olean lib/lean/Lean/Meta/Constructions/RecOn.olean.private lib/lean/Lean/Meta/Constructions/RecOn.olean.server +lib/lean/Lean/Meta/Constructions/SparseCasesOn.ilean +lib/lean/Lean/Meta/Constructions/SparseCasesOn.ir +lib/lean/Lean/Meta/Constructions/SparseCasesOn.olean +lib/lean/Lean/Meta/Constructions/SparseCasesOn.olean.private +lib/lean/Lean/Meta/Constructions/SparseCasesOn.olean.server lib/lean/Lean/Meta/CtorRecognizer.ilean lib/lean/Lean/Meta/CtorRecognizer.ir lib/lean/Lean/Meta/CtorRecognizer.olean @@ -5802,6 +6112,11 @@ lib/lean/Lean/Meta/GlobalInstances.ir lib/lean/Lean/Meta/GlobalInstances.olean lib/lean/Lean/Meta/GlobalInstances.olean.private lib/lean/Lean/Meta/GlobalInstances.olean.server +lib/lean/Lean/Meta/HasNotBit.ilean +lib/lean/Lean/Meta/HasNotBit.ir +lib/lean/Lean/Meta/HasNotBit.olean +lib/lean/Lean/Meta/HasNotBit.olean.private +lib/lean/Lean/Meta/HasNotBit.olean.server lib/lean/Lean/Meta/Hint.ilean lib/lean/Lean/Meta/Hint.ir lib/lean/Lean/Meta/Hint.olean @@ -5937,6 +6252,16 @@ lib/lean/Lean/Meta/Match/MatcherInfo.ir lib/lean/Lean/Meta/Match/MatcherInfo.olean lib/lean/Lean/Meta/Match/MatcherInfo.olean.private lib/lean/Lean/Meta/Match/MatcherInfo.olean.server +lib/lean/Lean/Meta/Match/SimpH.ilean +lib/lean/Lean/Meta/Match/SimpH.ir +lib/lean/Lean/Meta/Match/SimpH.olean +lib/lean/Lean/Meta/Match/SimpH.olean.private +lib/lean/Lean/Meta/Match/SimpH.olean.server +lib/lean/Lean/Meta/Match/SolveOverlap.ilean +lib/lean/Lean/Meta/Match/SolveOverlap.ir +lib/lean/Lean/Meta/Match/SolveOverlap.olean +lib/lean/Lean/Meta/Match/SolveOverlap.olean.private +lib/lean/Lean/Meta/Match/SolveOverlap.olean.server lib/lean/Lean/Meta/Match/Value.ilean lib/lean/Lean/Meta/Match/Value.ir lib/lean/Lean/Meta/Match/Value.olean @@ -5987,6 +6312,11 @@ lib/lean/Lean/Meta/PProdN.ir lib/lean/Lean/Meta/PProdN.olean lib/lean/Lean/Meta/PProdN.olean.private lib/lean/Lean/Meta/PProdN.olean.server +lib/lean/Lean/Meta/ProdN.ilean +lib/lean/Lean/Meta/ProdN.ir +lib/lean/Lean/Meta/ProdN.olean +lib/lean/Lean/Meta/ProdN.olean.private +lib/lean/Lean/Meta/ProdN.olean.server lib/lean/Lean/Meta/RecursorInfo.ilean lib/lean/Lean/Meta/RecursorInfo.ir lib/lean/Lean/Meta/RecursorInfo.olean @@ -6312,6 +6642,11 @@ lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Poly.ir lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Poly.olean lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Poly.olean.private lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Poly.olean.server +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Power.ilean +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Power.ir +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Power.olean +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Power.olean.private +lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Power.olean.server lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Proof.ilean lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Proof.ir lib/lean/Lean/Meta/Tactic/Grind/Arith/CommRing/Proof.olean @@ -6467,11 +6802,21 @@ lib/lean/Lean/Meta/Tactic/Grind/Arith/EvalNum.ir lib/lean/Lean/Meta/Tactic/Grind/Arith/EvalNum.olean lib/lean/Lean/Meta/Tactic/Grind/Arith/EvalNum.olean.private lib/lean/Lean/Meta/Tactic/Grind/Arith/EvalNum.olean.server +lib/lean/Lean/Meta/Tactic/Grind/Arith/FieldNormNum.ilean +lib/lean/Lean/Meta/Tactic/Grind/Arith/FieldNormNum.ir +lib/lean/Lean/Meta/Tactic/Grind/Arith/FieldNormNum.olean +lib/lean/Lean/Meta/Tactic/Grind/Arith/FieldNormNum.olean.private +lib/lean/Lean/Meta/Tactic/Grind/Arith/FieldNormNum.olean.server lib/lean/Lean/Meta/Tactic/Grind/Arith/Insts.ilean lib/lean/Lean/Meta/Tactic/Grind/Arith/Insts.ir lib/lean/Lean/Meta/Tactic/Grind/Arith/Insts.olean lib/lean/Lean/Meta/Tactic/Grind/Arith/Insts.olean.private lib/lean/Lean/Meta/Tactic/Grind/Arith/Insts.olean.server +lib/lean/Lean/Meta/Tactic/Grind/Arith/IsRelevant.ilean +lib/lean/Lean/Meta/Tactic/Grind/Arith/IsRelevant.ir +lib/lean/Lean/Meta/Tactic/Grind/Arith/IsRelevant.olean +lib/lean/Lean/Meta/Tactic/Grind/Arith/IsRelevant.olean.private +lib/lean/Lean/Meta/Tactic/Grind/Arith/IsRelevant.olean.server lib/lean/Lean/Meta/Tactic/Grind/Arith/Linear.ilean lib/lean/Lean/Meta/Tactic/Grind/Arith/Linear.ir lib/lean/Lean/Meta/Tactic/Grind/Arith/Linear.olean @@ -6482,6 +6827,11 @@ lib/lean/Lean/Meta/Tactic/Grind/Arith/Linear/Action.ir lib/lean/Lean/Meta/Tactic/Grind/Arith/Linear/Action.olean lib/lean/Lean/Meta/Tactic/Grind/Arith/Linear/Action.olean.private lib/lean/Lean/Meta/Tactic/Grind/Arith/Linear/Action.olean.server +lib/lean/Lean/Meta/Tactic/Grind/Arith/Linear/Den.ilean +lib/lean/Lean/Meta/Tactic/Grind/Arith/Linear/Den.ir +lib/lean/Lean/Meta/Tactic/Grind/Arith/Linear/Den.olean +lib/lean/Lean/Meta/Tactic/Grind/Arith/Linear/Den.olean.private +lib/lean/Lean/Meta/Tactic/Grind/Arith/Linear/Den.olean.server lib/lean/Lean/Meta/Tactic/Grind/Arith/Linear/DenoteExpr.ilean lib/lean/Lean/Meta/Tactic/Grind/Arith/Linear/DenoteExpr.ir lib/lean/Lean/Meta/Tactic/Grind/Arith/Linear/DenoteExpr.olean @@ -6597,36 +6947,6 @@ lib/lean/Lean/Meta/Tactic/Grind/Arith/ModelUtil.ir lib/lean/Lean/Meta/Tactic/Grind/Arith/ModelUtil.olean lib/lean/Lean/Meta/Tactic/Grind/Arith/ModelUtil.olean.private lib/lean/Lean/Meta/Tactic/Grind/Arith/ModelUtil.olean.server -lib/lean/Lean/Meta/Tactic/Grind/Arith/Offset.ilean -lib/lean/Lean/Meta/Tactic/Grind/Arith/Offset.ir -lib/lean/Lean/Meta/Tactic/Grind/Arith/Offset.olean -lib/lean/Lean/Meta/Tactic/Grind/Arith/Offset.olean.private -lib/lean/Lean/Meta/Tactic/Grind/Arith/Offset.olean.server -lib/lean/Lean/Meta/Tactic/Grind/Arith/Offset/Main.ilean -lib/lean/Lean/Meta/Tactic/Grind/Arith/Offset/Main.ir -lib/lean/Lean/Meta/Tactic/Grind/Arith/Offset/Main.olean -lib/lean/Lean/Meta/Tactic/Grind/Arith/Offset/Main.olean.private -lib/lean/Lean/Meta/Tactic/Grind/Arith/Offset/Main.olean.server -lib/lean/Lean/Meta/Tactic/Grind/Arith/Offset/Model.ilean -lib/lean/Lean/Meta/Tactic/Grind/Arith/Offset/Model.ir -lib/lean/Lean/Meta/Tactic/Grind/Arith/Offset/Model.olean -lib/lean/Lean/Meta/Tactic/Grind/Arith/Offset/Model.olean.private -lib/lean/Lean/Meta/Tactic/Grind/Arith/Offset/Model.olean.server -lib/lean/Lean/Meta/Tactic/Grind/Arith/Offset/Proof.ilean -lib/lean/Lean/Meta/Tactic/Grind/Arith/Offset/Proof.ir -lib/lean/Lean/Meta/Tactic/Grind/Arith/Offset/Proof.olean -lib/lean/Lean/Meta/Tactic/Grind/Arith/Offset/Proof.olean.private -lib/lean/Lean/Meta/Tactic/Grind/Arith/Offset/Proof.olean.server -lib/lean/Lean/Meta/Tactic/Grind/Arith/Offset/Types.ilean -lib/lean/Lean/Meta/Tactic/Grind/Arith/Offset/Types.ir -lib/lean/Lean/Meta/Tactic/Grind/Arith/Offset/Types.olean -lib/lean/Lean/Meta/Tactic/Grind/Arith/Offset/Types.olean.private -lib/lean/Lean/Meta/Tactic/Grind/Arith/Offset/Types.olean.server -lib/lean/Lean/Meta/Tactic/Grind/Arith/Offset/Util.ilean -lib/lean/Lean/Meta/Tactic/Grind/Arith/Offset/Util.ir -lib/lean/Lean/Meta/Tactic/Grind/Arith/Offset/Util.olean -lib/lean/Lean/Meta/Tactic/Grind/Arith/Offset/Util.olean.private -lib/lean/Lean/Meta/Tactic/Grind/Arith/Offset/Util.olean.server lib/lean/Lean/Meta/Tactic/Grind/Arith/Simproc.ilean lib/lean/Lean/Meta/Tactic/Grind/Arith/Simproc.ir lib/lean/Lean/Meta/Tactic/Grind/Arith/Simproc.olean @@ -6677,6 +6997,11 @@ lib/lean/Lean/Meta/Tactic/Grind/CheckResult.ir lib/lean/Lean/Meta/Tactic/Grind/CheckResult.olean lib/lean/Lean/Meta/Tactic/Grind/CheckResult.olean.private lib/lean/Lean/Meta/Tactic/Grind/CheckResult.olean.server +lib/lean/Lean/Meta/Tactic/Grind/CollectParams.ilean +lib/lean/Lean/Meta/Tactic/Grind/CollectParams.ir +lib/lean/Lean/Meta/Tactic/Grind/CollectParams.olean +lib/lean/Lean/Meta/Tactic/Grind/CollectParams.olean.private +lib/lean/Lean/Meta/Tactic/Grind/CollectParams.olean.server lib/lean/Lean/Meta/Tactic/Grind/Core.ilean lib/lean/Lean/Meta/Tactic/Grind/Core.ir lib/lean/Lean/Meta/Tactic/Grind/Core.olean @@ -6712,6 +7037,11 @@ lib/lean/Lean/Meta/Tactic/Grind/EMatchTheoremParam.ir lib/lean/Lean/Meta/Tactic/Grind/EMatchTheoremParam.olean lib/lean/Lean/Meta/Tactic/Grind/EMatchTheoremParam.olean.private lib/lean/Lean/Meta/Tactic/Grind/EMatchTheoremParam.olean.server +lib/lean/Lean/Meta/Tactic/Grind/EMatchTheoremPtr.ilean +lib/lean/Lean/Meta/Tactic/Grind/EMatchTheoremPtr.ir +lib/lean/Lean/Meta/Tactic/Grind/EMatchTheoremPtr.olean +lib/lean/Lean/Meta/Tactic/Grind/EMatchTheoremPtr.olean.private +lib/lean/Lean/Meta/Tactic/Grind/EMatchTheoremPtr.olean.server lib/lean/Lean/Meta/Tactic/Grind/EqResolution.ilean lib/lean/Lean/Meta/Tactic/Grind/EqResolution.ir lib/lean/Lean/Meta/Tactic/Grind/EqResolution.olean @@ -6732,11 +7062,26 @@ lib/lean/Lean/Meta/Tactic/Grind/ExtAttr.ir lib/lean/Lean/Meta/Tactic/Grind/ExtAttr.olean lib/lean/Lean/Meta/Tactic/Grind/ExtAttr.olean.private lib/lean/Lean/Meta/Tactic/Grind/ExtAttr.olean.server +lib/lean/Lean/Meta/Tactic/Grind/Filter.ilean +lib/lean/Lean/Meta/Tactic/Grind/Filter.ir +lib/lean/Lean/Meta/Tactic/Grind/Filter.olean +lib/lean/Lean/Meta/Tactic/Grind/Filter.olean.private +lib/lean/Lean/Meta/Tactic/Grind/Filter.olean.server +lib/lean/Lean/Meta/Tactic/Grind/Finish.ilean +lib/lean/Lean/Meta/Tactic/Grind/Finish.ir +lib/lean/Lean/Meta/Tactic/Grind/Finish.olean +lib/lean/Lean/Meta/Tactic/Grind/Finish.olean.private +lib/lean/Lean/Meta/Tactic/Grind/Finish.olean.server lib/lean/Lean/Meta/Tactic/Grind/ForallProp.ilean lib/lean/Lean/Meta/Tactic/Grind/ForallProp.ir lib/lean/Lean/Meta/Tactic/Grind/ForallProp.olean lib/lean/Lean/Meta/Tactic/Grind/ForallProp.olean.private lib/lean/Lean/Meta/Tactic/Grind/ForallProp.olean.server +lib/lean/Lean/Meta/Tactic/Grind/FunCC.ilean +lib/lean/Lean/Meta/Tactic/Grind/FunCC.ir +lib/lean/Lean/Meta/Tactic/Grind/FunCC.olean +lib/lean/Lean/Meta/Tactic/Grind/FunCC.olean.private +lib/lean/Lean/Meta/Tactic/Grind/FunCC.olean.server lib/lean/Lean/Meta/Tactic/Grind/Injection.ilean lib/lean/Lean/Meta/Tactic/Grind/Injection.ir lib/lean/Lean/Meta/Tactic/Grind/Injection.olean @@ -6897,11 +7242,6 @@ lib/lean/Lean/Meta/Tactic/Grind/RevertAll.ir lib/lean/Lean/Meta/Tactic/Grind/RevertAll.olean lib/lean/Lean/Meta/Tactic/Grind/RevertAll.olean.private lib/lean/Lean/Meta/Tactic/Grind/RevertAll.olean.server -lib/lean/Lean/Meta/Tactic/Grind/SearchM.ilean -lib/lean/Lean/Meta/Tactic/Grind/SearchM.ir -lib/lean/Lean/Meta/Tactic/Grind/SearchM.olean -lib/lean/Lean/Meta/Tactic/Grind/SearchM.olean.private -lib/lean/Lean/Meta/Tactic/Grind/SearchM.olean.server lib/lean/Lean/Meta/Tactic/Grind/Simp.ilean lib/lean/Lean/Meta/Tactic/Grind/Simp.ir lib/lean/Lean/Meta/Tactic/Grind/Simp.olean @@ -7392,21 +7732,6 @@ lib/lean/Lean/ParserCompiler/Attribute.ir lib/lean/Lean/ParserCompiler/Attribute.olean lib/lean/Lean/ParserCompiler/Attribute.olean.private lib/lean/Lean/ParserCompiler/Attribute.olean.server -lib/lean/Lean/PremiseSelection.ilean -lib/lean/Lean/PremiseSelection.ir -lib/lean/Lean/PremiseSelection.olean -lib/lean/Lean/PremiseSelection.olean.private -lib/lean/Lean/PremiseSelection.olean.server -lib/lean/Lean/PremiseSelection/Basic.ilean -lib/lean/Lean/PremiseSelection/Basic.ir -lib/lean/Lean/PremiseSelection/Basic.olean -lib/lean/Lean/PremiseSelection/Basic.olean.private -lib/lean/Lean/PremiseSelection/Basic.olean.server -lib/lean/Lean/PremiseSelection/MePo.ilean -lib/lean/Lean/PremiseSelection/MePo.ir -lib/lean/Lean/PremiseSelection/MePo.olean -lib/lean/Lean/PremiseSelection/MePo.olean.private -lib/lean/Lean/PremiseSelection/MePo.olean.server lib/lean/Lean/PrettyPrinter.ilean lib/lean/Lean/PrettyPrinter.ir lib/lean/Lean/PrettyPrinter.olean @@ -7647,6 +7972,16 @@ lib/lean/Lean/Server/InfoUtils.ir lib/lean/Lean/Server/InfoUtils.olean lib/lean/Lean/Server/InfoUtils.olean.private lib/lean/Lean/Server/InfoUtils.olean.server +lib/lean/Lean/Server/Logging.ilean +lib/lean/Lean/Server/Logging.ir +lib/lean/Lean/Server/Logging.olean +lib/lean/Lean/Server/Logging.olean.private +lib/lean/Lean/Server/Logging.olean.server +lib/lean/Lean/Server/ProtocolOverview.ilean +lib/lean/Lean/Server/ProtocolOverview.ir +lib/lean/Lean/Server/ProtocolOverview.olean +lib/lean/Lean/Server/ProtocolOverview.olean.private +lib/lean/Lean/Server/ProtocolOverview.olean.server lib/lean/Lean/Server/References.ilean lib/lean/Lean/Server/References.ir lib/lean/Lean/Server/References.olean @@ -7887,6 +8222,11 @@ lib/lean/Lean/Util/PPExt.ir lib/lean/Lean/Util/PPExt.olean lib/lean/Lean/Util/PPExt.olean.private lib/lean/Lean/Util/PPExt.olean.server +lib/lean/Lean/Util/ParamMinimizer.ilean +lib/lean/Lean/Util/ParamMinimizer.ir +lib/lean/Lean/Util/ParamMinimizer.olean +lib/lean/Lean/Util/ParamMinimizer.olean.private +lib/lean/Lean/Util/ParamMinimizer.olean.server lib/lean/Lean/Util/Path.ilean lib/lean/Lean/Util/Path.ir lib/lean/Lean/Util/Path.olean @@ -8199,6 +8539,16 @@ lib/lean/Std/Data/DTreeMap/Internal/WF/Lemmas.ir lib/lean/Std/Data/DTreeMap/Internal/WF/Lemmas.olean lib/lean/Std/Data/DTreeMap/Internal/WF/Lemmas.olean.private lib/lean/Std/Data/DTreeMap/Internal/WF/Lemmas.olean.server +lib/lean/Std/Data/DTreeMap/Internal/Zipper.ilean +lib/lean/Std/Data/DTreeMap/Internal/Zipper.ir +lib/lean/Std/Data/DTreeMap/Internal/Zipper.olean +lib/lean/Std/Data/DTreeMap/Internal/Zipper.olean.private +lib/lean/Std/Data/DTreeMap/Internal/Zipper.olean.server +lib/lean/Std/Data/DTreeMap/Iterator.ilean +lib/lean/Std/Data/DTreeMap/Iterator.ir +lib/lean/Std/Data/DTreeMap/Iterator.olean +lib/lean/Std/Data/DTreeMap/Iterator.olean.private +lib/lean/Std/Data/DTreeMap/Iterator.olean.server lib/lean/Std/Data/DTreeMap/Lemmas.ilean lib/lean/Std/Data/DTreeMap/Lemmas.ir lib/lean/Std/Data/DTreeMap/Lemmas.olean @@ -8219,16 +8569,31 @@ lib/lean/Std/Data/DTreeMap/Raw/Basic.ir lib/lean/Std/Data/DTreeMap/Raw/Basic.olean lib/lean/Std/Data/DTreeMap/Raw/Basic.olean.private lib/lean/Std/Data/DTreeMap/Raw/Basic.olean.server +lib/lean/Std/Data/DTreeMap/Raw/Iterator.ilean +lib/lean/Std/Data/DTreeMap/Raw/Iterator.ir +lib/lean/Std/Data/DTreeMap/Raw/Iterator.olean +lib/lean/Std/Data/DTreeMap/Raw/Iterator.olean.private +lib/lean/Std/Data/DTreeMap/Raw/Iterator.olean.server lib/lean/Std/Data/DTreeMap/Raw/Lemmas.ilean lib/lean/Std/Data/DTreeMap/Raw/Lemmas.ir lib/lean/Std/Data/DTreeMap/Raw/Lemmas.olean lib/lean/Std/Data/DTreeMap/Raw/Lemmas.olean.private lib/lean/Std/Data/DTreeMap/Raw/Lemmas.olean.server +lib/lean/Std/Data/DTreeMap/Raw/Slice.ilean +lib/lean/Std/Data/DTreeMap/Raw/Slice.ir +lib/lean/Std/Data/DTreeMap/Raw/Slice.olean +lib/lean/Std/Data/DTreeMap/Raw/Slice.olean.private +lib/lean/Std/Data/DTreeMap/Raw/Slice.olean.server lib/lean/Std/Data/DTreeMap/Raw/WF.ilean lib/lean/Std/Data/DTreeMap/Raw/WF.ir lib/lean/Std/Data/DTreeMap/Raw/WF.olean lib/lean/Std/Data/DTreeMap/Raw/WF.olean.private lib/lean/Std/Data/DTreeMap/Raw/WF.olean.server +lib/lean/Std/Data/DTreeMap/Slice.ilean +lib/lean/Std/Data/DTreeMap/Slice.ir +lib/lean/Std/Data/DTreeMap/Slice.olean +lib/lean/Std/Data/DTreeMap/Slice.olean.private +lib/lean/Std/Data/DTreeMap/Slice.olean.server lib/lean/Std/Data/ExtDHashMap.ilean lib/lean/Std/Data/ExtDHashMap.ir lib/lean/Std/Data/ExtDHashMap.olean @@ -8449,11 +8814,6 @@ lib/lean/Std/Data/Iterators/Combinators/Monadic/StepSize.ir lib/lean/Std/Data/Iterators/Combinators/Monadic/StepSize.olean lib/lean/Std/Data/Iterators/Combinators/Monadic/StepSize.olean.private lib/lean/Std/Data/Iterators/Combinators/Monadic/StepSize.olean.server -lib/lean/Std/Data/Iterators/Combinators/Monadic/Take.ilean -lib/lean/Std/Data/Iterators/Combinators/Monadic/Take.ir -lib/lean/Std/Data/Iterators/Combinators/Monadic/Take.olean -lib/lean/Std/Data/Iterators/Combinators/Monadic/Take.olean.private -lib/lean/Std/Data/Iterators/Combinators/Monadic/Take.olean.server lib/lean/Std/Data/Iterators/Combinators/Monadic/TakeWhile.ilean lib/lean/Std/Data/Iterators/Combinators/Monadic/TakeWhile.ir lib/lean/Std/Data/Iterators/Combinators/Monadic/TakeWhile.olean @@ -8469,11 +8829,6 @@ lib/lean/Std/Data/Iterators/Combinators/StepSize.ir lib/lean/Std/Data/Iterators/Combinators/StepSize.olean lib/lean/Std/Data/Iterators/Combinators/StepSize.olean.private lib/lean/Std/Data/Iterators/Combinators/StepSize.olean.server -lib/lean/Std/Data/Iterators/Combinators/Take.ilean -lib/lean/Std/Data/Iterators/Combinators/Take.ir -lib/lean/Std/Data/Iterators/Combinators/Take.olean -lib/lean/Std/Data/Iterators/Combinators/Take.olean.private -lib/lean/Std/Data/Iterators/Combinators/Take.olean.server lib/lean/Std/Data/Iterators/Combinators/TakeWhile.ilean *** 634 LINES SKIPPED ***