diff options
Diffstat (limited to 'math/lean4/pkg-plist')
| -rw-r--r-- | math/lean4/pkg-plist | 91 |
1 files changed, 83 insertions, 8 deletions
diff --git a/math/lean4/pkg-plist b/math/lean4/pkg-plist index 75fc4ce6be58..fee7268e93e1 100644 --- a/math/lean4/pkg-plist +++ b/math/lean4/pkg-plist @@ -100,6 +100,8 @@ lib/lean/Init/Data/Char.ilean lib/lean/Init/Data/Char.olean lib/lean/Init/Data/Char/Basic.ilean lib/lean/Init/Data/Char/Basic.olean +lib/lean/Init/Data/Char/Lemmas.ilean +lib/lean/Init/Data/Char/Lemmas.olean lib/lean/Init/Data/Fin.ilean lib/lean/Init/Data/Fin.olean lib/lean/Init/Data/Fin/Basic.ilean @@ -134,6 +136,8 @@ lib/lean/Init/Data/Int.ilean lib/lean/Init/Data/Int.olean lib/lean/Init/Data/Int/Basic.ilean lib/lean/Init/Data/Int/Basic.olean +lib/lean/Init/Data/Int/Bitwise/Lemmas.ilean +lib/lean/Init/Data/Int/Bitwise/Lemmas.olean lib/lean/Init/Data/Int/Bitwise.ilean lib/lean/Init/Data/Int/Bitwise.olean lib/lean/Init/Data/Int/DivMod.ilean @@ -144,6 +148,8 @@ lib/lean/Init/Data/Int/Gcd.ilean lib/lean/Init/Data/Int/Gcd.olean lib/lean/Init/Data/Int/Lemmas.ilean lib/lean/Init/Data/Int/Lemmas.olean +lib/lean/Init/Data/List/TakeDrop.ilean +lib/lean/Init/Data/List/TakeDrop.olean lib/lean/Init/Data/Int/Order.ilean lib/lean/Init/Data/Int/Order.olean lib/lean/Init/Data/Int/Pow.ilean @@ -230,6 +236,8 @@ lib/lean/Init/Data/String/Basic.ilean lib/lean/Init/Data/String/Basic.olean 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/Sum.ilean lib/lean/Init/Data/Sum.olean lib/lean/Init/Data/ToString.ilean @@ -244,12 +252,24 @@ lib/lean/Init/Data/UInt/Basic.ilean lib/lean/Init/Data/UInt/Basic.olean lib/lean/Init/Data/UInt/Log2.ilean lib/lean/Init/Data/UInt/Log2.olean +lib/lean/Init/Data/UInt/Lemmas.ilean +lib/lean/Init/Data/UInt/Lemmas.olean lib/lean/Init/Dynamic.ilean lib/lean/Init/Dynamic.olean lib/lean/Init/Ext.ilean lib/lean/Init/Ext.olean lib/lean/Init/GetElem.ilean lib/lean/Init/GetElem.olean +lib/lean/Init/Grind.ilean +lib/lean/Init/Grind.olean +lib/lean/Init/Grind/Cases.ilean +lib/lean/Init/Grind/Cases.olean +lib/lean/Init/Grind/Lemmas.ilean +lib/lean/Init/Grind/Lemmas.olean +lib/lean/Init/Grind/Norm.ilean +lib/lean/Init/Grind/Norm.olean +lib/lean/Init/Grind/Tactics.ilean +lib/lean/Init/Grind/Tactics.olean lib/lean/Init/Guard.ilean lib/lean/Init/Guard.olean lib/lean/Init/Hints.ilean @@ -440,6 +460,8 @@ lib/lean/Lake/DSL.ilean lib/lean/Lake/DSL.olean lib/lean/Lake/DSL/Attributes.ilean lib/lean/Lake/DSL/Attributes.olean +lib/lean/Lake/DSL/AttributesCore.ilean +lib/lean/Lake/DSL/AttributesCore.olean lib/lean/Lake/DSL/Config.ilean lib/lean/Lake/DSL/Config.olean lib/lean/Lake/DSL/DeclUtil.ilean @@ -528,6 +550,8 @@ lib/lean/Lake/Util/Git.ilean lib/lean/Lake/Util/Git.olean lib/lean/Lake/Util/IO.ilean lib/lean/Lake/Util/IO.olean +lib/lean/Lake/Util/JsonObject.ilean +lib/lean/Lake/Util/JsonObject.olean lib/lean/Lake/Util/Lift.ilean lib/lean/Lake/Util/Lift.olean lib/lean/Lake/Util/List.ilean @@ -544,8 +568,6 @@ lib/lean/Lake/Util/Name.ilean lib/lean/Lake/Util/Name.olean lib/lean/Lake/Util/NativeLib.ilean lib/lean/Lake/Util/NativeLib.olean -lib/lean/Lake/Util/Newline.ilean -lib/lean/Lake/Util/Newline.olean lib/lean/Lake/Util/Opaque.ilean lib/lean/Lake/Util/Opaque.olean lib/lean/Lake/Util/OrdHashSet.ilean @@ -564,10 +586,14 @@ lib/lean/Lake/Util/Sugar.ilean lib/lean/Lake/Util/Sugar.olean lib/lean/Lake/Util/Task.ilean lib/lean/Lake/Util/Task.olean +lib/lean/Lake/Util/Version.ilean +lib/lean/Lake/Util/Version.olean lib/lean/Lake/Version.ilean lib/lean/Lake/Version.olean lib/lean/Lean.ilean lib/lean/Lean.olean +lib/lean/Lean/AddDecl.ilean +lib/lean/Lean/AddDecl.olean lib/lean/Lean/Attributes.ilean lib/lean/Lean/Attributes.olean lib/lean/Lean/AuxRecursor.ilean @@ -1436,6 +1462,24 @@ lib/lean/Lean/Meta/Tactic/FunInd.ilean lib/lean/Lean/Meta/Tactic/FunInd.olean lib/lean/Lean/Meta/Tactic/Generalize.ilean lib/lean/Lean/Meta/Tactic/Generalize.olean +lib/lean/Lean/Meta/Tactic/Grind.ilean +lib/lean/Lean/Meta/Tactic/Grind.olean +lib/lean/Lean/Meta/Tactic/Grind/Attr.ilean +lib/lean/Lean/Meta/Tactic/Grind/Attr.olean +lib/lean/Lean/Meta/Tactic/Grind/Cases.ilean +lib/lean/Lean/Meta/Tactic/Grind/Cases.olean +lib/lean/Lean/Meta/Tactic/Grind/Core.ilean +lib/lean/Lean/Meta/Tactic/Grind/Core.olean +lib/lean/Lean/Meta/Tactic/Grind/Injection.ilean +lib/lean/Lean/Meta/Tactic/Grind/Injection.olean +lib/lean/Lean/Meta/Tactic/Grind/Preprocessor.ilean +lib/lean/Lean/Meta/Tactic/Grind/Preprocessor.olean +lib/lean/Lean/Meta/Tactic/Grind/RevertAll.ilean +lib/lean/Lean/Meta/Tactic/Grind/RevertAll.olean +lib/lean/Lean/Meta/Tactic/Grind/Types.ilean +lib/lean/Lean/Meta/Tactic/Grind/Types.olean +lib/lean/Lean/Meta/Tactic/Grind/Util.ilean +lib/lean/Lean/Meta/Tactic/Grind/Util.olean lib/lean/Lean/Meta/Tactic/IndependentOf.ilean lib/lean/Lean/Meta/Tactic/IndependentOf.olean lib/lean/Lean/Meta/Tactic/Induction.ilean @@ -1829,6 +1873,7 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Init/Data/Channel.lean %%DATADIR%%/src/lean/Init/Data/Char.lean %%DATADIR%%/src/lean/Init/Data/Char/Basic.lean +%%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/Fold.lean @@ -1847,6 +1892,7 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Init/Data/Int.lean %%DATADIR%%/src/lean/Init/Data/Int/Basic.lean %%DATADIR%%/src/lean/Init/Data/Int/Bitwise.lean +%%DATADIR%%/src/lean/Init/Data/Int/Bitwise/Lemmas.lean %%DATADIR%%/src/lean/Init/Data/Int/DivMod.lean %%DATADIR%%/src/lean/Init/Data/Int/DivModLemmas.lean %%DATADIR%%/src/lean/Init/Data/Int/Gcd.lean @@ -1859,6 +1905,7 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Init/Data/List/Control.lean %%DATADIR%%/src/lean/Init/Data/List/Impl.lean %%DATADIR%%/src/lean/Init/Data/List/Lemmas.lean +%%DATADIR%%/src/lean/Init/Data/List/TakeDrop.lean %%DATADIR%%/src/lean/Init/Data/Nat.lean %%DATADIR%%/src/lean/Init/Data/Nat/Basic.lean %%DATADIR%%/src/lean/Init/Data/Nat/Bitwise.lean @@ -1894,16 +1941,23 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Init/Data/String.lean %%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/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/Lemmas.lean %%DATADIR%%/src/lean/Init/Data/UInt/Log2.lean %%DATADIR%%/src/lean/Init/Dynamic.lean %%DATADIR%%/src/lean/Init/Ext.lean %%DATADIR%%/src/lean/Init/GetElem.lean +%%DATADIR%%/src/lean/Init/Grind.lean +%%DATADIR%%/src/lean/Init/Grind/Cases.lean +%%DATADIR%%/src/lean/Init/Grind/Lemmas.lean +%%DATADIR%%/src/lean/Init/Grind/Norm.lean +%%DATADIR%%/src/lean/Init/Grind/Tactics.lean %%DATADIR%%/src/lean/Init/Guard.lean %%DATADIR%%/src/lean/Init/Hints.lean %%DATADIR%%/src/lean/Init/MacroTrace.lean @@ -1941,6 +1995,7 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Init/WF.lean %%DATADIR%%/src/lean/Init/WFTactics.lean %%DATADIR%%/src/lean/Lean.lean +%%DATADIR%%/src/lean/Lean/AddDecl.lean %%DATADIR%%/src/lean/Lean/Attributes.lean %%DATADIR%%/src/lean/Lean/AuxRecursor.lean %%DATADIR%%/src/lean/Lean/BuiltinDocAttr.lean @@ -2375,6 +2430,15 @@ share/lean/lean.mk %%DATADIR%%/src/lean/Lean/Meta/Tactic/FVarSubst.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/FunInd.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Generalize.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Attr.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Cases.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Core.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Injection.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Preprocessor.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/RevertAll.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Types.lean +%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Util.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/IndependentOf.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Induction.lean %%DATADIR%%/src/lean/Lean/Meta/Tactic/Injection.lean @@ -2605,6 +2669,7 @@ share/lean/lean.mk %%DATADIR%%/src/lean/lake/Lake/Config/WorkspaceConfig.lean %%DATADIR%%/src/lean/lake/Lake/DSL.lean %%DATADIR%%/src/lean/lake/Lake/DSL/Attributes.lean +%%DATADIR%%/src/lean/lake/Lake/DSL/AttributesCore.lean %%DATADIR%%/src/lean/lake/Lake/DSL/Config.lean %%DATADIR%%/src/lean/lake/Lake/DSL/DeclUtil.lean %%DATADIR%%/src/lean/lake/Lake/DSL/Extensions.lean @@ -2649,6 +2714,7 @@ share/lean/lean.mk %%DATADIR%%/src/lean/lake/Lake/Util/FilePath.lean %%DATADIR%%/src/lean/lake/Lake/Util/Git.lean %%DATADIR%%/src/lean/lake/Lake/Util/IO.lean +%%DATADIR%%/src/lean/lake/Lake/Util/JsonObject.lean %%DATADIR%%/src/lean/lake/Lake/Util/Lift.lean %%DATADIR%%/src/lean/lake/Lake/Util/List.lean %%DATADIR%%/src/lean/lake/Lake/Util/Lock.lean @@ -2657,7 +2723,6 @@ share/lean/lean.mk %%DATADIR%%/src/lean/lake/Lake/Util/Message.lean %%DATADIR%%/src/lean/lake/Lake/Util/Name.lean %%DATADIR%%/src/lean/lake/Lake/Util/NativeLib.lean -%%DATADIR%%/src/lean/lake/Lake/Util/Newline.lean %%DATADIR%%/src/lean/lake/Lake/Util/Opaque.lean %%DATADIR%%/src/lean/lake/Lake/Util/OrdHashSet.lean %%DATADIR%%/src/lean/lake/Lake/Util/OrderedTagAttribute.lean @@ -2667,6 +2732,7 @@ share/lean/lean.mk %%DATADIR%%/src/lean/lake/Lake/Util/StoreInsts.lean %%DATADIR%%/src/lean/lake/Lake/Util/Sugar.lean %%DATADIR%%/src/lean/lake/Lake/Util/Task.lean +%%DATADIR%%/src/lean/lake/Lake/Util/Version.lean %%DATADIR%%/src/lean/lake/Lake/Version.lean %%DATADIR%%/src/lean/lake/README.md %%DATADIR%%/src/lean/lake/lakefile.lean @@ -2681,6 +2747,19 @@ share/lean/lean.mk %%DATADIR%%/src/lean/lake/tests/buildArgs/lakefile.lean %%DATADIR%%/src/lean/lake/tests/clone/test/Main.lean %%DATADIR%%/src/lean/lake/tests/clone/test/lakefile.lean +%%DATADIR%%/src/lean/lake/tests/driver/Test.lean +%%DATADIR%%/src/lean/lake/tests/driver/dep-invalid.lean +%%DATADIR%%/src/lean/lake/tests/driver/dep-unknown.lean +%%DATADIR%%/src/lean/lake/tests/driver/dep.lean +%%DATADIR%%/src/lean/lake/tests/driver/dep/lakefile.lean +%%DATADIR%%/src/lean/lake/tests/driver/driver.lean +%%DATADIR%%/src/lean/lake/tests/driver/exe.lean +%%DATADIR%%/src/lean/lake/tests/driver/lib.lean +%%DATADIR%%/src/lean/lake/tests/driver/none.lean +%%DATADIR%%/src/lean/lake/tests/driver/runner.lean +%%DATADIR%%/src/lean/lake/tests/driver/script.lean +%%DATADIR%%/src/lean/lake/tests/driver/two.lean +%%DATADIR%%/src/lean/lake/tests/driver/unknown.lean %%DATADIR%%/src/lean/lake/tests/globs/TBA.lean %%DATADIR%%/src/lean/lake/tests/globs/TBA/Eulerian.lean %%DATADIR%%/src/lean/lake/tests/globs/TBA/Eulerian/A.lean @@ -2731,13 +2810,9 @@ share/lean/lean.mk %%DATADIR%%/src/lean/lake/tests/reversion/Hello.lean %%DATADIR%%/src/lean/lake/tests/reversion/Main.lean %%DATADIR%%/src/lean/lake/tests/reversion/lakefile.lean -%%DATADIR%%/src/lean/lake/tests/test/exe.lean -%%DATADIR%%/src/lean/lake/tests/test/none.lean -%%DATADIR%%/src/lean/lake/tests/test/script.lean -%%DATADIR%%/src/lean/lake/tests/test/test.lean -%%DATADIR%%/src/lean/lake/tests/test/two.lean %%DATADIR%%/src/lean/lake/tests/toml/README.md %%DATADIR%%/src/lean/lake/tests/toml/Test.lean +%%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 |