Date: Mon, 2 Sep 2024 07:54:57 GMT From: Yuri Victorovich <yuri@FreeBSD.org> To: ports-committers@FreeBSD.org, dev-commits-ports-all@FreeBSD.org, dev-commits-ports-main@FreeBSD.org Subject: git: 1fde20b526dd - main - math/lean4: update 4.10.0 =?utf-8?Q?=E2=86=92?= 4.11.0 Message-ID: <202409020754.4827svgJ012015@gitrepo.freebsd.org>
next in thread | raw e-mail | index | archive | help
The branch main has been updated by yuri: URL: https://cgit.FreeBSD.org/ports/commit/?id=1fde20b526ddc12811e0af7ee6a71e1f732eaf5b commit 1fde20b526ddc12811e0af7ee6a71e1f732eaf5b Author: Yuri Victorovich <yuri@FreeBSD.org> AuthorDate: 2024-09-02 07:54:32 +0000 Commit: Yuri Victorovich <yuri@FreeBSD.org> CommitDate: 2024-09-02 07:54:45 +0000 math/lean4: update 4.10.0 → 4.11.0 --- math/lean4/Makefile | 2 +- math/lean4/distinfo | 6 +- math/lean4/pkg-plist | 220 ++++++++++++++++++++++++++++++++++++++++++++++++--- 3 files changed, 215 insertions(+), 13 deletions(-) diff --git a/math/lean4/Makefile b/math/lean4/Makefile index 562dad632944..abfc3004d07b 100644 --- a/math/lean4/Makefile +++ b/math/lean4/Makefile @@ -1,6 +1,6 @@ PORTNAME= lean4 DISTVERSIONPREFIX= v -DISTVERSION= 4.10.0 +DISTVERSION= 4.11.0 CATEGORIES= math lang devel # lean4 is primarily a math theorem prover, but it is also a language and a development environment MAINTAINER= yuri@FreeBSD.org diff --git a/math/lean4/distinfo b/math/lean4/distinfo index 1ca0f069d7a4..fd56f3893df9 100644 --- a/math/lean4/distinfo +++ b/math/lean4/distinfo @@ -1,3 +1,3 @@ -TIMESTAMP = 1722411891 -SHA256 (leanprover-lean4-v4.10.0_GH0.tar.gz) = dee5d1dbcea924fa3f4500c1f4854ea5953f471e3600dac71421c742c844b094 -SIZE (leanprover-lean4-v4.10.0_GH0.tar.gz) = 25013155 +TIMESTAMP = 1725254182 +SHA256 (leanprover-lean4-v4.11.0_GH0.tar.gz) = 8b7fc8e71e107250c7bbf911eb1f450379d874857a26236577aaa624dd5962b5 +SIZE (leanprover-lean4-v4.11.0_GH0.tar.gz) = 25790812 diff --git a/math/lean4/pkg-plist b/math/lean4/pkg-plist index 65859221ae90..365f371356e4 100644 --- a/math/lean4/pkg-plist +++ b/math/lean4/pkg-plist @@ -54,6 +54,8 @@ lib/lean/Init/Data/AC.ilean lib/lean/Init/Data/AC.olean lib/lean/Init/Data/Array.ilean lib/lean/Init/Data/Array.olean +lib/lean/Init/Data/Array/Attach.ilean +lib/lean/Init/Data/Array/Attach.olean lib/lean/Init/Data/Array/Basic.ilean lib/lean/Init/Data/Array/Basic.olean lib/lean/Init/Data/Array/BasicAux.ilean @@ -74,6 +76,10 @@ lib/lean/Init/Data/Array/Subarray.ilean lib/lean/Init/Data/Array/Subarray.olean lib/lean/Init/Data/Array/Subarray/Split.ilean lib/lean/Init/Data/Array/Subarray/Split.olean +lib/lean/Init/Data/Array/TakeDrop.ilean +lib/lean/Init/Data/Array/TakeDrop.olean +lib/lean/Init/Data/BEq.ilean +lib/lean/Init/Data/BEq.olean lib/lean/Init/Data/Basic.ilean lib/lean/Init/Data/Basic.olean lib/lean/Init/Data/BitVec.ilean @@ -106,6 +112,8 @@ lib/lean/Init/Data/Fin.ilean lib/lean/Init/Data/Fin.olean lib/lean/Init/Data/Fin/Basic.ilean lib/lean/Init/Data/Fin/Basic.olean +lib/lean/Init/Data/Fin/Bitwise.ilean +lib/lean/Init/Data/Fin/Bitwise.olean lib/lean/Init/Data/Fin/Fold.ilean lib/lean/Init/Data/Fin/Fold.olean lib/lean/Init/Data/Fin/Iterate.ilean @@ -154,20 +162,48 @@ lib/lean/Init/Data/Int/Pow.ilean lib/lean/Init/Data/Int/Pow.olean lib/lean/Init/Data/List.ilean lib/lean/Init/Data/List.olean +lib/lean/Init/Data/List/Attach.ilean +lib/lean/Init/Data/List/Attach.olean lib/lean/Init/Data/List/Basic.ilean lib/lean/Init/Data/List/Basic.olean lib/lean/Init/Data/List/BasicAux.ilean lib/lean/Init/Data/List/BasicAux.olean lib/lean/Init/Data/List/Control.ilean lib/lean/Init/Data/List/Control.olean +lib/lean/Init/Data/List/Count.ilean +lib/lean/Init/Data/List/Count.olean +lib/lean/Init/Data/List/Erase.ilean +lib/lean/Init/Data/List/Erase.olean +lib/lean/Init/Data/List/Find.ilean +lib/lean/Init/Data/List/Find.olean lib/lean/Init/Data/List/Impl.ilean lib/lean/Init/Data/List/Impl.olean lib/lean/Init/Data/List/Lemmas.ilean lib/lean/Init/Data/List/Lemmas.olean +lib/lean/Init/Data/List/MinMax.ilean +lib/lean/Init/Data/List/MinMax.olean +lib/lean/Init/Data/List/Monadic.ilean +lib/lean/Init/Data/List/Monadic.olean +lib/lean/Init/Data/List/Nat.ilean +lib/lean/Init/Data/List/Nat.olean +lib/lean/Init/Data/List/Nat/Basic.ilean +lib/lean/Init/Data/List/Nat/Basic.olean +lib/lean/Init/Data/List/Nat/Pairwise.ilean +lib/lean/Init/Data/List/Nat/Pairwise.olean +lib/lean/Init/Data/List/Nat/Range.ilean +lib/lean/Init/Data/List/Nat/Range.olean +lib/lean/Init/Data/List/Nat/TakeDrop.ilean +lib/lean/Init/Data/List/Nat/TakeDrop.olean lib/lean/Init/Data/List/Notation.ilean lib/lean/Init/Data/List/Notation.olean +lib/lean/Init/Data/List/Pairwise.ilean +lib/lean/Init/Data/List/Pairwise.olean +lib/lean/Init/Data/List/Sublist.ilean +lib/lean/Init/Data/List/Sublist.olean lib/lean/Init/Data/List/TakeDrop.ilean lib/lean/Init/Data/List/TakeDrop.olean +lib/lean/Init/Data/List/Zip.ilean +lib/lean/Init/Data/List/Zip.olean lib/lean/Init/Data/Nat.ilean lib/lean/Init/Data/Nat.olean lib/lean/Init/Data/Nat/Basic.ilean @@ -240,6 +276,8 @@ lib/lean/Init/Data/String/Extra.ilean lib/lean/Init/Data/String/Extra.olean lib/lean/Init/Data/String/Lemmas.ilean lib/lean/Init/Data/String/Lemmas.olean +lib/lean/Init/Data/Subtype.ilean +lib/lean/Init/Data/Subtype.olean lib/lean/Init/Data/Sum.ilean lib/lean/Init/Data/Sum.olean lib/lean/Init/Data/ToString.ilean @@ -252,6 +290,8 @@ lib/lean/Init/Data/UInt.ilean lib/lean/Init/Data/UInt.olean lib/lean/Init/Data/UInt/Basic.ilean lib/lean/Init/Data/UInt/Basic.olean +lib/lean/Init/Data/UInt/Bitwise.ilean +lib/lean/Init/Data/UInt/Bitwise.olean lib/lean/Init/Data/UInt/Lemmas.ilean lib/lean/Init/Data/UInt/Lemmas.olean lib/lean/Init/Data/UInt/Log2.ilean @@ -1092,14 +1132,22 @@ lib/lean/Lean/Elab/PreDefinition/Structural/Eqns.ilean lib/lean/Lean/Elab/PreDefinition/Structural/Eqns.olean lib/lean/Lean/Elab/PreDefinition/Structural/FindRecArg.ilean lib/lean/Lean/Elab/PreDefinition/Structural/FindRecArg.olean +lib/lean/Lean/Elab/PreDefinition/Structural/IndGroupInfo.ilean +lib/lean/Lean/Elab/PreDefinition/Structural/IndGroupInfo.olean lib/lean/Lean/Elab/PreDefinition/Structural/IndPred.ilean lib/lean/Lean/Elab/PreDefinition/Structural/IndPred.olean lib/lean/Lean/Elab/PreDefinition/Structural/Main.ilean lib/lean/Lean/Elab/PreDefinition/Structural/Main.olean lib/lean/Lean/Elab/PreDefinition/Structural/Preprocess.ilean lib/lean/Lean/Elab/PreDefinition/Structural/Preprocess.olean +lib/lean/Lean/Elab/PreDefinition/Structural/RecArgInfo.ilean +lib/lean/Lean/Elab/PreDefinition/Structural/RecArgInfo.olean lib/lean/Lean/Elab/PreDefinition/Structural/SmartUnfolding.ilean lib/lean/Lean/Elab/PreDefinition/Structural/SmartUnfolding.olean +lib/lean/Lean/Elab/PreDefinition/TerminationArgument.ilean +lib/lean/Lean/Elab/PreDefinition/TerminationArgument.olean +lib/lean/Lean/Elab/PreDefinition/TerminationHint.ilean +lib/lean/Lean/Elab/PreDefinition/TerminationHint.olean lib/lean/Lean/Elab/PreDefinition/WF.ilean lib/lean/Lean/Elab/PreDefinition/WF.olean lib/lean/Lean/Elab/PreDefinition/WF/Eqns.ilean @@ -1118,10 +1166,6 @@ lib/lean/Lean/Elab/PreDefinition/WF/Preprocess.ilean lib/lean/Lean/Elab/PreDefinition/WF/Preprocess.olean lib/lean/Lean/Elab/PreDefinition/WF/Rel.ilean lib/lean/Lean/Elab/PreDefinition/WF/Rel.olean -lib/lean/Lean/Elab/PreDefinition/WF/TerminationArgument.ilean -lib/lean/Lean/Elab/PreDefinition/WF/TerminationArgument.olean -lib/lean/Lean/Elab/PreDefinition/WF/TerminationHint.ilean -lib/lean/Lean/Elab/PreDefinition/WF/TerminationHint.olean lib/lean/Lean/Elab/Print.ilean lib/lean/Lean/Elab/Print.olean lib/lean/Lean/Elab/Quotation.ilean @@ -1178,6 +1222,8 @@ lib/lean/Lean/Elab/Tactic/Conv/Unfold.ilean lib/lean/Lean/Elab/Tactic/Conv/Unfold.olean lib/lean/Lean/Elab/Tactic/Delta.ilean lib/lean/Lean/Elab/Tactic/Delta.olean +lib/lean/Lean/Elab/Tactic/DiscrTreeKey.ilean +lib/lean/Lean/Elab/Tactic/DiscrTreeKey.olean lib/lean/Lean/Elab/Tactic/Doc.ilean lib/lean/Lean/Elab/Tactic/Doc.olean lib/lean/Lean/Elab/Tactic/ElabTerm.ilean @@ -1270,6 +1316,8 @@ lib/lean/Lean/Language/Basic.ilean lib/lean/Lean/Language/Basic.olean lib/lean/Lean/Language/Lean.ilean lib/lean/Lean/Language/Lean.olean +lib/lean/Lean/Language/Lean/Types.ilean +lib/lean/Lean/Language/Lean/Types.olean lib/lean/Lean/LazyInitExtension.ilean lib/lean/Lean/LazyInitExtension.olean lib/lean/Lean/Level.ilean @@ -1286,6 +1334,8 @@ lib/lean/Lean/Linter/Deprecated.ilean lib/lean/Lean/Linter/Deprecated.olean lib/lean/Lean/Linter/MissingDocs.ilean lib/lean/Lean/Linter/MissingDocs.olean +lib/lean/Lean/Linter/Omit.ilean +lib/lean/Lean/Linter/Omit.olean lib/lean/Lean/Linter/UnusedVariables.ilean lib/lean/Lean/Linter/UnusedVariables.olean lib/lean/Lean/Linter/Util.ilean @@ -1338,6 +1388,10 @@ lib/lean/Lean/Meta/Constructions.ilean lib/lean/Lean/Meta/Constructions.olean lib/lean/Lean/Meta/Constructions/BRecOn.ilean lib/lean/Lean/Meta/Constructions/BRecOn.olean +lib/lean/Lean/Meta/Constructions/CasesOn.ilean +lib/lean/Lean/Meta/Constructions/CasesOn.olean +lib/lean/Lean/Meta/Constructions/NoConfusion.ilean +lib/lean/Lean/Meta/Constructions/NoConfusion.olean lib/lean/Lean/Meta/Constructions/RecOn.ilean lib/lean/Lean/Meta/Constructions/RecOn.olean lib/lean/Lean/Meta/CtorRecognizer.ilean @@ -1430,6 +1484,8 @@ lib/lean/Lean/Meta/Offset.ilean lib/lean/Lean/Meta/Offset.olean lib/lean/Lean/Meta/PPGoal.ilean lib/lean/Lean/Meta/PPGoal.olean +lib/lean/Lean/Meta/PProdN.ilean +lib/lean/Lean/Meta/PProdN.olean lib/lean/Lean/Meta/RecursorInfo.ilean lib/lean/Lean/Meta/RecursorInfo.olean lib/lean/Lean/Meta/Reduce.ilean @@ -1552,6 +1608,8 @@ lib/lean/Lean/Meta/Tactic/Simp/Attr.ilean lib/lean/Lean/Meta/Tactic/Simp/Attr.olean lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs.ilean lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs.olean +lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Array.ilean +lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Array.olean lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/BitVec.ilean lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/BitVec.olean lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Char.ilean @@ -1562,6 +1620,8 @@ lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Fin.ilean lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Fin.olean lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Int.ilean lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Int.olean +lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/List.ilean +lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/List.olean lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.ilean lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.olean lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/String.ilean @@ -1754,6 +1814,8 @@ lib/lean/Lean/ToExpr.ilean lib/lean/Lean/ToExpr.olean lib/lean/Lean/Util.ilean lib/lean/Lean/Util.olean +lib/lean/Lean/Util/CollectAxioms.ilean +lib/lean/Lean/Util/CollectAxioms.olean lib/lean/Lean/Util/CollectFVars.ilean lib/lean/Lean/Util/CollectFVars.olean lib/lean/Lean/Util/CollectLevelParams.ilean @@ -1790,6 +1852,8 @@ lib/lean/Lean/Util/MonadBacktrack.ilean lib/lean/Lean/Util/MonadBacktrack.olean lib/lean/Lean/Util/MonadCache.ilean lib/lean/Lean/Util/MonadCache.olean +lib/lean/Lean/Util/NumObjs.ilean +lib/lean/Lean/Util/NumObjs.olean lib/lean/Lean/Util/OccursCheck.ilean lib/lean/Lean/Util/OccursCheck.olean lib/lean/Lean/Util/PPExt.ilean @@ -1814,6 +1878,10 @@ lib/lean/Lean/Util/ReplaceLevel.ilean lib/lean/Lean/Util/ReplaceLevel.olean lib/lean/Lean/Util/SCC.ilean lib/lean/Lean/Util/SCC.olean +lib/lean/Lean/Util/SafeExponentiation.ilean +lib/lean/Lean/Util/SafeExponentiation.olean +lib/lean/Lean/Util/SearchPath.ilean +lib/lean/Lean/Util/SearchPath.olean lib/lean/Lean/Util/ShareCommon.ilean lib/lean/Lean/Util/ShareCommon.olean lib/lean/Lean/Util/Sorry.ilean @@ -1842,6 +1910,72 @@ lib/lean/Lean/Widget/UserWidget.ilean lib/lean/Lean/Widget/UserWidget.olean lib/lean/Std.ilean lib/lean/Std.olean +lib/lean/Std/Data.ilean +lib/lean/Std/Data.olean +lib/lean/Std/Data/DHashMap.ilean +lib/lean/Std/Data/DHashMap.olean +lib/lean/Std/Data/DHashMap/AdditionalOperations.ilean +lib/lean/Std/Data/DHashMap/AdditionalOperations.olean +lib/lean/Std/Data/DHashMap/Basic.ilean +lib/lean/Std/Data/DHashMap/Basic.olean +lib/lean/Std/Data/DHashMap/Internal/AssocList/Basic.ilean +lib/lean/Std/Data/DHashMap/Internal/AssocList/Basic.olean +lib/lean/Std/Data/DHashMap/Internal/AssocList/Lemmas.ilean +lib/lean/Std/Data/DHashMap/Internal/AssocList/Lemmas.olean +lib/lean/Std/Data/DHashMap/Internal/Defs.ilean +lib/lean/Std/Data/DHashMap/Internal/Defs.olean +lib/lean/Std/Data/DHashMap/Internal/Index.ilean +lib/lean/Std/Data/DHashMap/Internal/Index.olean +lib/lean/Std/Data/DHashMap/Internal/List/Associative.ilean +lib/lean/Std/Data/DHashMap/Internal/List/Associative.olean +lib/lean/Std/Data/DHashMap/Internal/List/Defs.ilean +lib/lean/Std/Data/DHashMap/Internal/List/Defs.olean +lib/lean/Std/Data/DHashMap/Internal/List/HashesTo.ilean +lib/lean/Std/Data/DHashMap/Internal/List/HashesTo.olean +lib/lean/Std/Data/DHashMap/Internal/List/Pairwise.ilean +lib/lean/Std/Data/DHashMap/Internal/List/Pairwise.olean +lib/lean/Std/Data/DHashMap/Internal/List/Perm.ilean +lib/lean/Std/Data/DHashMap/Internal/List/Perm.olean +lib/lean/Std/Data/DHashMap/Internal/List/Sublist.ilean +lib/lean/Std/Data/DHashMap/Internal/List/Sublist.olean +lib/lean/Std/Data/DHashMap/Internal/Model.ilean +lib/lean/Std/Data/DHashMap/Internal/Model.olean +lib/lean/Std/Data/DHashMap/Internal/Raw.ilean +lib/lean/Std/Data/DHashMap/Internal/Raw.olean +lib/lean/Std/Data/DHashMap/Internal/RawLemmas.ilean +lib/lean/Std/Data/DHashMap/Internal/RawLemmas.olean +lib/lean/Std/Data/DHashMap/Internal/WF.ilean +lib/lean/Std/Data/DHashMap/Internal/WF.olean +lib/lean/Std/Data/DHashMap/Lemmas.ilean +lib/lean/Std/Data/DHashMap/Lemmas.olean +lib/lean/Std/Data/DHashMap/Raw.ilean +lib/lean/Std/Data/DHashMap/Raw.olean +lib/lean/Std/Data/DHashMap/RawDef.ilean +lib/lean/Std/Data/DHashMap/RawDef.olean +lib/lean/Std/Data/DHashMap/RawLemmas.ilean +lib/lean/Std/Data/DHashMap/RawLemmas.olean +lib/lean/Std/Data/HashMap.ilean +lib/lean/Std/Data/HashMap.olean +lib/lean/Std/Data/HashMap/AdditionalOperations.ilean +lib/lean/Std/Data/HashMap/AdditionalOperations.olean +lib/lean/Std/Data/HashMap/Basic.ilean +lib/lean/Std/Data/HashMap/Basic.olean +lib/lean/Std/Data/HashMap/Lemmas.ilean +lib/lean/Std/Data/HashMap/Lemmas.olean +lib/lean/Std/Data/HashMap/Raw.ilean +lib/lean/Std/Data/HashMap/Raw.olean +lib/lean/Std/Data/HashMap/RawLemmas.ilean +lib/lean/Std/Data/HashMap/RawLemmas.olean +lib/lean/Std/Data/HashSet.ilean +lib/lean/Std/Data/HashSet.olean +lib/lean/Std/Data/HashSet/Basic.ilean +lib/lean/Std/Data/HashSet/Basic.olean +lib/lean/Std/Data/HashSet/Lemmas.ilean +lib/lean/Std/Data/HashSet/Lemmas.olean +lib/lean/Std/Data/HashSet/Raw.ilean +lib/lean/Std/Data/HashSet/Raw.olean +lib/lean/Std/Data/HashSet/RawLemmas.ilean +lib/lean/Std/Data/HashSet/RawLemmas.olean lib/lean/libInit.a lib/lean/libInit_shared.so lib/lean/libLake.a @@ -1875,6 +2009,7 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Init/Data.lean %%DATADIR%%/src/lean/Init/Data/AC.lean %%DATADIR%%/src/lean/Init/Data/Array.lean +%%DATADIR%%/src/lean/Init/Data/Array/Attach.lean %%DATADIR%%/src/lean/Init/Data/Array/Basic.lean %%DATADIR%%/src/lean/Init/Data/Array/BasicAux.lean %%DATADIR%%/src/lean/Init/Data/Array/BinSearch.lean @@ -1885,6 +2020,8 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Init/Data/Array/QSort.lean %%DATADIR%%/src/lean/Init/Data/Array/Subarray.lean %%DATADIR%%/src/lean/Init/Data/Array/Subarray/Split.lean +%%DATADIR%%/src/lean/Init/Data/Array/TakeDrop.lean +%%DATADIR%%/src/lean/Init/Data/BEq.lean %%DATADIR%%/src/lean/Init/Data/Basic.lean %%DATADIR%%/src/lean/Init/Data/BitVec.lean %%DATADIR%%/src/lean/Init/Data/BitVec/Basic.lean @@ -1901,6 +2038,7 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Init/Data/Char/Lemmas.lean %%DATADIR%%/src/lean/Init/Data/Fin.lean %%DATADIR%%/src/lean/Init/Data/Fin/Basic.lean +%%DATADIR%%/src/lean/Init/Data/Fin/Bitwise.lean %%DATADIR%%/src/lean/Init/Data/Fin/Fold.lean %%DATADIR%%/src/lean/Init/Data/Fin/Iterate.lean %%DATADIR%%/src/lean/Init/Data/Fin/Lemmas.lean @@ -1925,13 +2063,27 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Init/Data/Int/Order.lean %%DATADIR%%/src/lean/Init/Data/Int/Pow.lean %%DATADIR%%/src/lean/Init/Data/List.lean +%%DATADIR%%/src/lean/Init/Data/List/Attach.lean %%DATADIR%%/src/lean/Init/Data/List/Basic.lean %%DATADIR%%/src/lean/Init/Data/List/BasicAux.lean %%DATADIR%%/src/lean/Init/Data/List/Control.lean +%%DATADIR%%/src/lean/Init/Data/List/Count.lean +%%DATADIR%%/src/lean/Init/Data/List/Erase.lean +%%DATADIR%%/src/lean/Init/Data/List/Find.lean %%DATADIR%%/src/lean/Init/Data/List/Impl.lean %%DATADIR%%/src/lean/Init/Data/List/Lemmas.lean +%%DATADIR%%/src/lean/Init/Data/List/MinMax.lean +%%DATADIR%%/src/lean/Init/Data/List/Monadic.lean +%%DATADIR%%/src/lean/Init/Data/List/Nat.lean +%%DATADIR%%/src/lean/Init/Data/List/Nat/Basic.lean +%%DATADIR%%/src/lean/Init/Data/List/Nat/Pairwise.lean +%%DATADIR%%/src/lean/Init/Data/List/Nat/Range.lean +%%DATADIR%%/src/lean/Init/Data/List/Nat/TakeDrop.lean %%DATADIR%%/src/lean/Init/Data/List/Notation.lean +%%DATADIR%%/src/lean/Init/Data/List/Pairwise.lean +%%DATADIR%%/src/lean/Init/Data/List/Sublist.lean %%DATADIR%%/src/lean/Init/Data/List/TakeDrop.lean +%%DATADIR%%/src/lean/Init/Data/List/Zip.lean %%DATADIR%%/src/lean/Init/Data/Nat.lean %%DATADIR%%/src/lean/Init/Data/Nat/Basic.lean %%DATADIR%%/src/lean/Init/Data/Nat/Bitwise.lean @@ -1968,12 +2120,14 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Init/Data/String/Basic.lean %%DATADIR%%/src/lean/Init/Data/String/Extra.lean %%DATADIR%%/src/lean/Init/Data/String/Lemmas.lean +%%DATADIR%%/src/lean/Init/Data/Subtype.lean %%DATADIR%%/src/lean/Init/Data/Sum.lean %%DATADIR%%/src/lean/Init/Data/ToString.lean %%DATADIR%%/src/lean/Init/Data/ToString/Basic.lean %%DATADIR%%/src/lean/Init/Data/ToString/Macro.lean %%DATADIR%%/src/lean/Init/Data/UInt.lean %%DATADIR%%/src/lean/Init/Data/UInt/Basic.lean +%%DATADIR%%/src/lean/Init/Data/UInt/Bitwise.lean %%DATADIR%%/src/lean/Init/Data/UInt/Lemmas.lean %%DATADIR%%/src/lean/Init/Data/UInt/Log2.lean %%DATADIR%%/src/lean/Init/Dynamic.lean @@ -2266,10 +2420,14 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/Structural/Basic.lean %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/Structural/Eqns.lean %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/Structural/FindRecArg.lean +%%DATADIR%%/src/lean/Lean/Elab/PreDefinition/Structural/IndGroupInfo.lean %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/Structural/IndPred.lean %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/Structural/Main.lean %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/Structural/Preprocess.lean +%%DATADIR%%/src/lean/Lean/Elab/PreDefinition/Structural/RecArgInfo.lean %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/Structural/SmartUnfolding.lean +%%DATADIR%%/src/lean/Lean/Elab/PreDefinition/TerminationArgument.lean +%%DATADIR%%/src/lean/Lean/Elab/PreDefinition/TerminationHint.lean %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/WF.lean %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/WF/Eqns.lean %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/WF/Fix.lean @@ -2279,8 +2437,6 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/WF/PackMutual.lean %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/WF/Preprocess.lean %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/WF/Rel.lean -%%DATADIR%%/src/lean/Lean/Elab/PreDefinition/WF/TerminationArgument.lean -%%DATADIR%%/src/lean/Lean/Elab/PreDefinition/WF/TerminationHint.lean %%DATADIR%%/src/lean/Lean/Elab/Print.lean %%DATADIR%%/src/lean/Lean/Elab/Quotation.lean %%DATADIR%%/src/lean/Lean/Elab/Quotation/Precheck.lean @@ -2309,6 +2465,7 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Elab/Tactic/Conv/Simp.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic/Conv/Unfold.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic/Delta.lean +%%DATADIR%%/src/lean/Lean/Elab/Tactic/DiscrTreeKey.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic/Doc.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic/ElabTerm.lean %%DATADIR%%/src/lean/Lean/Elab/Tactic/Ext.lean @@ -2355,6 +2512,7 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/LabelAttribute.lean %%DATADIR%%/src/lean/Lean/Language/Basic.lean %%DATADIR%%/src/lean/Lean/Language/Lean.lean +%%DATADIR%%/src/lean/Lean/Language/Lean/Types.lean %%DATADIR%%/src/lean/Lean/LazyInitExtension.lean %%DATADIR%%/src/lean/Lean/Level.lean %%DATADIR%%/src/lean/Lean/Linter.lean @@ -2363,6 +2521,7 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Linter/ConstructorAsVariable.lean %%DATADIR%%/src/lean/Lean/Linter/Deprecated.lean %%DATADIR%%/src/lean/Lean/Linter/MissingDocs.lean +%%DATADIR%%/src/lean/Lean/Linter/Omit.lean %%DATADIR%%/src/lean/Lean/Linter/UnusedVariables.lean %%DATADIR%%/src/lean/Lean/Linter/Util.lean %%DATADIR%%/src/lean/Lean/LoadDynlib.lean @@ -2389,6 +2548,8 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Meta/CongrTheorems.lean %%DATADIR%%/src/lean/Lean/Meta/Constructions.lean %%DATADIR%%/src/lean/Lean/Meta/Constructions/BRecOn.lean +%%DATADIR%%/src/lean/Lean/Meta/Constructions/CasesOn.lean +%%DATADIR%%/src/lean/Lean/Meta/Constructions/NoConfusion.lean %%DATADIR%%/src/lean/Lean/Meta/Constructions/RecOn.lean %%DATADIR%%/src/lean/Lean/Meta/CtorRecognizer.lean %%DATADIR%%/src/lean/Lean/Meta/DecLevel.lean @@ -2435,6 +2596,7 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Meta/NatInstTesters.lean %%DATADIR%%/src/lean/Lean/Meta/Offset.lean %%DATADIR%%/src/lean/Lean/Meta/PPGoal.lean +%%DATADIR%%/src/lean/Lean/Meta/PProdN.lean %%DATADIR%%/src/lean/Lean/Meta/RecursorInfo.lean %%DATADIR%%/src/lean/Lean/Meta/Reduce.lean %%DATADIR%%/src/lean/Lean/Meta/ReduceEval.lean @@ -2496,11 +2658,13 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/Attr.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Array.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/BitVec.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Char.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Core.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Fin.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Int.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/List.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/String.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/UInt.lean @@ -2598,6 +2762,7 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Syntax.lean %%DATADIR%%/src/lean/Lean/ToExpr.lean %%DATADIR%%/src/lean/Lean/Util.lean +%%DATADIR%%/src/lean/Lean/Util/CollectAxioms.lean %%DATADIR%%/src/lean/Lean/Util/CollectFVars.lean %%DATADIR%%/src/lean/Lean/Util/CollectLevelParams.lean %%DATADIR%%/src/lean/Lean/Util/CollectMVars.lean @@ -2616,6 +2781,7 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Util/LeanOptions.lean %%DATADIR%%/src/lean/Lean/Util/MonadBacktrack.lean %%DATADIR%%/src/lean/Lean/Util/MonadCache.lean +%%DATADIR%%/src/lean/Lean/Util/NumObjs.lean %%DATADIR%%/src/lean/Lean/Util/OccursCheck.lean %%DATADIR%%/src/lean/Lean/Util/PPExt.lean %%DATADIR%%/src/lean/Lean/Util/Path.lean @@ -2628,6 +2794,8 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Util/ReplaceExpr.lean %%DATADIR%%/src/lean/Lean/Util/ReplaceLevel.lean %%DATADIR%%/src/lean/Lean/Util/SCC.lean +%%DATADIR%%/src/lean/Lean/Util/SafeExponentiation.lean +%%DATADIR%%/src/lean/Lean/Util/SearchPath.lean %%DATADIR%%/src/lean/Lean/Util/ShareCommon.lean %%DATADIR%%/src/lean/Lean/Util/Sorry.lean %%DATADIR%%/src/lean/Lean/Util/TestExtern.lean @@ -2643,6 +2811,39 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Widget/UserWidget.lean %%DATADIR%%/src/lean/Leanc.lean %%DATADIR%%/src/lean/Std.lean +%%DATADIR%%/src/lean/Std/Data.lean +%%DATADIR%%/src/lean/Std/Data/DHashMap.lean +%%DATADIR%%/src/lean/Std/Data/DHashMap/AdditionalOperations.lean +%%DATADIR%%/src/lean/Std/Data/DHashMap/Basic.lean +%%DATADIR%%/src/lean/Std/Data/DHashMap/Internal/AssocList/Basic.lean +%%DATADIR%%/src/lean/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean +%%DATADIR%%/src/lean/Std/Data/DHashMap/Internal/Defs.lean +%%DATADIR%%/src/lean/Std/Data/DHashMap/Internal/Index.lean +%%DATADIR%%/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean +%%DATADIR%%/src/lean/Std/Data/DHashMap/Internal/List/Defs.lean +%%DATADIR%%/src/lean/Std/Data/DHashMap/Internal/List/HashesTo.lean +%%DATADIR%%/src/lean/Std/Data/DHashMap/Internal/List/Pairwise.lean +%%DATADIR%%/src/lean/Std/Data/DHashMap/Internal/List/Perm.lean +%%DATADIR%%/src/lean/Std/Data/DHashMap/Internal/List/Sublist.lean +%%DATADIR%%/src/lean/Std/Data/DHashMap/Internal/Model.lean +%%DATADIR%%/src/lean/Std/Data/DHashMap/Internal/Raw.lean +%%DATADIR%%/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean +%%DATADIR%%/src/lean/Std/Data/DHashMap/Internal/WF.lean +%%DATADIR%%/src/lean/Std/Data/DHashMap/Lemmas.lean +%%DATADIR%%/src/lean/Std/Data/DHashMap/Raw.lean +%%DATADIR%%/src/lean/Std/Data/DHashMap/RawDef.lean +%%DATADIR%%/src/lean/Std/Data/DHashMap/RawLemmas.lean +%%DATADIR%%/src/lean/Std/Data/HashMap.lean +%%DATADIR%%/src/lean/Std/Data/HashMap/AdditionalOperations.lean +%%DATADIR%%/src/lean/Std/Data/HashMap/Basic.lean +%%DATADIR%%/src/lean/Std/Data/HashMap/Lemmas.lean +%%DATADIR%%/src/lean/Std/Data/HashMap/Raw.lean +%%DATADIR%%/src/lean/Std/Data/HashMap/RawLemmas.lean +%%DATADIR%%/src/lean/Std/Data/HashSet.lean +%%DATADIR%%/src/lean/Std/Data/HashSet/Basic.lean +%%DATADIR%%/src/lean/Std/Data/HashSet/Lemmas.lean +%%DATADIR%%/src/lean/Std/Data/HashSet/Raw.lean +%%DATADIR%%/src/lean/Std/Data/HashSet/RawLemmas.lean %%DATADIR%%/src/lean/lake/Lake.lean %%DATADIR%%/src/lean/lake/Lake/Build.lean %%DATADIR%%/src/lean/lake/Lake/Build/Actions.lean @@ -2818,6 +3019,10 @@ share/lean/lean.mk %%DATADIR%%/src/lean/lake/tests/lock/Nop.lean %%DATADIR%%/src/lean/lake/tests/lock/Wait.lean %%DATADIR%%/src/lean/lake/tests/lock/lakefile.lean +%%DATADIR%%/src/lean/lake/tests/logLevel/Log/Error.lean +%%DATADIR%%/src/lean/lake/tests/logLevel/Log/Info.lean +%%DATADIR%%/src/lean/lake/tests/logLevel/Log/Warning.lean +%%DATADIR%%/src/lean/lake/tests/logLevel/lakefile.lean %%DATADIR%%/src/lean/lake/tests/manifest/bar/lakefile.lean %%DATADIR%%/src/lean/lake/tests/manifest/foo/lakefile.lean %%DATADIR%%/src/lean/lake/tests/manifest/lakefile.lean @@ -2857,6 +3062,3 @@ share/lean/lean.mk %%DATADIR%%/src/lean/lake/tests/trace/Foo.lean %%DATADIR%%/src/lean/lake/tests/translateConfig/out.expected.lean %%DATADIR%%/src/lean/lake/tests/translateConfig/source.lean -%%DATADIR%%/src/lean/lake/tests/wfail/Warn.lean -%%DATADIR%%/src/lean/lake/tests/wfail/lakefile.lean -@dir lib/lean/Std
Want to link to this message? Use this URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?202409020754.4827svgJ012015>