)]}' { "commit": "66b47a843b10091fd4f667044950731a599cba66", "tree": "0371c5fe05c40781ecc440b7dd621e5f2da03f3d", "parents": [ "cff19d7edf87b7d0754d9b14f8afe35c62c00173" ], "author": { "name": "Kim Morrison", "email": "kim@tqft.net", "time": "Thu Mar 20 15:35:40 2025 +1100" }, "committer": { "name": "Kim Morrison", "email": "kim@tqft.net", "time": "Mon Mar 24 10:30:32 2025 +1100" }, "message": "feat: deprecate Array.mkArray in favour of Array.replicate\n", "tree_diff": [ { "type": "modify", "old_id": "0d3b7a6269406b59fd21e7eb4325b5a93666a172", "old_mode": 33188, "old_path": "src/Init/Data/Array/Attach.lean", "new_id": "8239e7f8324abc0f56276c0edcc21238331ba4b6", "new_mode": 33188, "new_path": "src/Init/Data/Array/Attach.lean" }, { "type": "modify", "old_id": "052a94bf29b384901e55503639c1eddbc8141059", "old_mode": 33188, "old_path": "src/Init/Data/Array/Basic.lean", "new_id": "1280cd9045895025ee38ce872d687a653d13c7c4", "new_mode": 33188, "new_path": "src/Init/Data/Array/Basic.lean" }, { "type": "modify", "old_id": "957e9758cac0b5c46f3664f35e7fed08a73ef2a4", "old_mode": 33188, "old_path": "src/Init/Data/Array/Count.lean", "new_id": "d1ec631af21ee80743459451195ef2b9bab24623", "new_mode": 33188, "new_path": "src/Init/Data/Array/Count.lean" }, { "type": "modify", "old_id": "6a6f576999a5dc0332e4f3bdcbb6dd34ed1a2264", "old_mode": 33188, "old_path": "src/Init/Data/Array/Erase.lean", "new_id": "c7ddcfba4e7948043c9cedb0d01841b4cca28d93", "new_mode": 33188, "new_path": "src/Init/Data/Array/Erase.lean" }, { "type": "modify", "old_id": "1976c105e9709001ac69885a9e065349825c6afc", "old_mode": 33188, "old_path": "src/Init/Data/Array/Extract.lean", "new_id": "b399426669a28d2e02ef07127d3f0d3f9d47a6a7", "new_mode": 33188, "new_path": "src/Init/Data/Array/Extract.lean" }, { "type": "modify", "old_id": "695708dfc2399392d8aed3567c58b2cf56cf9253", "old_mode": 33188, "old_path": "src/Init/Data/Array/Find.lean", "new_id": "e3598283f65264bf39d7927379422b86ca464046", "new_mode": 33188, "new_path": "src/Init/Data/Array/Find.lean" }, { "type": "modify", "old_id": "65e3be26ca5f2fbb982088eb9b2124a71eb60506", "old_mode": 33188, "old_path": "src/Init/Data/Array/Lemmas.lean", "new_id": "c48ea603509477fbae661817629cbb837bc91301", "new_mode": 33188, "new_path": "src/Init/Data/Array/Lemmas.lean" }, { "type": "modify", "old_id": "80aabb07e1ccf7bd12f2cc7ce647a4e7cf4b9a2f", "old_mode": 33188, "old_path": "src/Init/Data/Array/MapIdx.lean", "new_id": "19c59a50470ad85af0979abe739000070d7ceaea", "new_mode": 33188, "new_path": "src/Init/Data/Array/MapIdx.lean" }, { "type": "modify", "old_id": "9fea34d774af085fd305003d0ecc88c96d870412", "old_mode": 33188, "old_path": "src/Init/Data/Array/Zip.lean", "new_id": "08e3a03c92abc13d2f710982f646ed12c0503999", "new_mode": 33188, "new_path": "src/Init/Data/Array/Zip.lean" }, { "type": "modify", "old_id": "46a98a858a0b13218cfcc7403c31bf8b9e7e7f5a", "old_mode": 33188, "old_path": "src/Init/Data/List/ToArray.lean", "new_id": "64725a333216de36e4ef81b17b6672a1e87e2a73", "new_mode": 33188, "new_path": "src/Init/Data/List/ToArray.lean" }, { "type": "modify", "old_id": "52a5fe75a25c8f784f1efd2d6c5da07393258d09", "old_mode": 33188, "old_path": "src/Init/Data/Vector/Attach.lean", "new_id": "b3aaa2532223500d549d05cc132c80a9e08cf546", "new_mode": 33188, "new_path": "src/Init/Data/Vector/Attach.lean" }, { "type": "modify", "old_id": "0031b4d30ed350bcc98d4a739a5646fc7ac1aad1", "old_mode": 33188, "old_path": "src/Init/Data/Vector/Basic.lean", "new_id": "95695c259592ddc365ef6b96d269662907af43b0", "new_mode": 33188, "new_path": "src/Init/Data/Vector/Basic.lean" }, { "type": "modify", "old_id": "238d9c7b020f63c9a5a1fa91bc487884f1b8c43f", "old_mode": 33188, "old_path": "src/Init/Data/Vector/Count.lean", "new_id": "583f14c97a0fb2e03020a265bbfbe19c54531240", "new_mode": 33188, "new_path": "src/Init/Data/Vector/Count.lean" }, { "type": "modify", "old_id": "4eb7e9f976cf571b4389c5e40fa75a25b227644c", "old_mode": 33188, "old_path": "src/Init/Data/Vector/Erase.lean", "new_id": "834b7e6fca07c30ef3a81541968c90e61fe0b3d6", "new_mode": 33188, "new_path": "src/Init/Data/Vector/Erase.lean" }, { "type": "modify", "old_id": "88f70b9dd20c26b141f6a96cb3284600dd295a15", "old_mode": 33188, "old_path": "src/Init/Data/Vector/Extract.lean", "new_id": "b5b7eeef77203dff0a3f7c4a0fe47d71673bf336", "new_mode": 33188, "new_path": "src/Init/Data/Vector/Extract.lean" }, { "type": "modify", "old_id": "05b235123f1b462e09414bb4e84f9ea4e636d2c0", "old_mode": 33188, "old_path": "src/Init/Data/Vector/Find.lean", "new_id": "8594b0124a0774b4965ad0d727aad37fae4fa1a1", "new_mode": 33188, "new_path": "src/Init/Data/Vector/Find.lean" }, { "type": "modify", "old_id": "6e7e8eee99cad1ec4b3e2e2a6c54d79bc6241a3f", "old_mode": 33188, "old_path": "src/Init/Data/Vector/Lemmas.lean", "new_id": "f47a87b4c3828093527e3789835e2171c3458bf1", "new_mode": 33188, "new_path": "src/Init/Data/Vector/Lemmas.lean" }, { "type": "modify", "old_id": "df7ab6ef59f9209bc877e78684bb3e5988ec8f81", "old_mode": 33188, "old_path": "src/Init/Data/Vector/MapIdx.lean", "new_id": "cfd1d8de9eff1f9d2c6f3ab8e9b709f610d3a58b", "new_mode": 33188, "new_path": "src/Init/Data/Vector/MapIdx.lean" }, { "type": "modify", "old_id": "491b2c4cc8293f1469409d3ad25a8a900d302002", "old_mode": 33188, "old_path": "src/Init/Data/Vector/Zip.lean", "new_id": "273184961066c5b37346df0d34f183ce84d4f6ee", "new_mode": 33188, "new_path": "src/Init/Data/Vector/Zip.lean" }, { "type": "modify", "old_id": "04dc7527b50bf91f031b5b6baa9fa52e8ec599a0", "old_mode": 33188, "old_path": "src/Lean/Compiler/IR/ExpandResetReuse.lean", "new_id": "dbfdbdf72f4c7aa95601c1b6b75e8e60ad55d37a", "new_mode": 33188, "new_path": "src/Lean/Compiler/IR/ExpandResetReuse.lean" }, { "type": "modify", "old_id": "5d216c29796b3ff8cfdb323de4f7e9eca1b9657b", "old_mode": 33188, "old_path": "src/Lean/Compiler/LCNF/FixedParams.lean", "new_id": "490e1dcbc01ee2f95da18292c23d4e0203cc0267", "new_mode": 33188, "new_path": "src/Lean/Compiler/LCNF/FixedParams.lean" }, { "type": "modify", "old_id": "d6cb3f222bda358c0cd855de475f2a75e3c9a7d9", "old_mode": 33188, "old_path": "src/Lean/Compiler/LCNF/Simp/DiscrM.lean", "new_id": "614a08bb5ec440f86af981071ebe1731ad114d8c", "new_mode": 33188, "new_path": "src/Lean/Compiler/LCNF/Simp/DiscrM.lean" }, { "type": "modify", "old_id": "b63556c355c7cbfe30efcffeee58672ad906ec04", "old_mode": 33188, "old_path": "src/Lean/Compiler/LCNF/SpecInfo.lean", "new_id": "3571d7fda322d1e03574510a8d4da157ba8fce82", "new_mode": 33188, "new_path": "src/Lean/Compiler/LCNF/SpecInfo.lean" }, { "type": "modify", "old_id": "584d7ea9338bc385460789e1ebcb7ae93303c905", "old_mode": 33188, "old_path": "src/Lean/Data/Array.lean", "new_id": "e65c958899eccf50e2f1a5e947e9cb44c7cc6f53", "new_mode": 33188, "new_path": "src/Lean/Data/Array.lean" }, { "type": "modify", "old_id": "d3ab316f6bfcf7f93dc1ffa0bcdd9017989e0138", "old_mode": 33188, "old_path": "src/Lean/Data/FuzzyMatching.lean", "new_id": "07be4d0adbba5be6c849c1a660a77565def935c1", "new_mode": 33188, "new_path": "src/Lean/Data/FuzzyMatching.lean" }, { "type": "modify", "old_id": "c6b2380731d756bab96cb07bd346b582c0525b74", "old_mode": 33188, "old_path": "src/Lean/Data/PersistentHashMap.lean", "new_id": "90df37be75f6c2d1b78bce9366f9f35443064e13", "new_mode": 33188, "new_path": "src/Lean/Data/PersistentHashMap.lean" }, { "type": "modify", "old_id": "6c385ed6590977b434a74676c887db3a4c82c94b", "old_mode": 33188, "old_path": "src/Lean/Elab/ComputedFields.lean", "new_id": "8194b8cca6ab62cb07163a83dea6f94e03f10f8b", "new_mode": 33188, "new_path": "src/Lean/Elab/ComputedFields.lean" }, { "type": "modify", "old_id": "0be758f61cc17ebca7c70c94571ae4a4f36c62d8", "old_mode": 33188, "old_path": "src/Lean/Elab/MutualInductive.lean", "new_id": "20209e732e10b4d7bdb20961341213423dd5caae", "new_mode": 33188, "new_path": "src/Lean/Elab/MutualInductive.lean" }, { "type": "modify", "old_id": "556223d7c15c09524f5e904e3d2bfb84ad34c13c", "old_mode": 33188, "old_path": "src/Lean/Elab/PreDefinition/FixedParams.lean", "new_id": "bffb6561e04e4e3bc24d8cc075c092f02586b651", "new_mode": 33188, "new_path": "src/Lean/Elab/PreDefinition/FixedParams.lean" }, { "type": "modify", "old_id": "53a6a37e767a1538e7b36574398185a1da0a48bd", "old_mode": 33188, "old_path": "src/Lean/Elab/PreDefinition/Structural/BRecOn.lean", "new_id": "f801d4336e4137056cbc4c1cd05a05c003562161", "new_mode": 33188, "new_path": "src/Lean/Elab/PreDefinition/Structural/BRecOn.lean" }, { "type": "modify", "old_id": "36ad05395f5318c06c99824934929d40f3618d2a", "old_mode": 33188, "old_path": "src/Lean/Elab/PreDefinition/Structural/Basic.lean", "new_id": "ff21d94f459c8d92518b4b4d4dc866a8d5c7f098", "new_mode": 33188, "new_path": "src/Lean/Elab/PreDefinition/Structural/Basic.lean" }, { "type": "modify", "old_id": "ada75b2f7c5ffc0a76610f661b01d806b79bc91e", "old_mode": 33188, "old_path": "src/Lean/Elab/PreDefinition/Structural/RecArgInfo.lean", "new_id": "64182d0e1922103b615def157469abbf6bc63a85", "new_mode": 33188, "new_path": "src/Lean/Elab/PreDefinition/Structural/RecArgInfo.lean" }, { "type": "modify", "old_id": "0311aee000fb5b2d914ddef35f6df522d9802f33", "old_mode": 33188, "old_path": "src/Lean/Elab/PreDefinition/WF/Fix.lean", "new_id": "6a8482209636509d14e900f7987622a4f3f489a4", "new_mode": 33188, "new_path": "src/Lean/Elab/PreDefinition/WF/Fix.lean" }, { "type": "modify", "old_id": "5fa3d6c6b996bffae114a1982dad5a6132eebb3f", "old_mode": 33188, "old_path": "src/Lean/Elab/PreDefinition/WF/GuessLex.lean", "new_id": "a56521493434268708b9278615c30eafa89b5a03", "new_mode": 33188, "new_path": "src/Lean/Elab/PreDefinition/WF/GuessLex.lean" }, { "type": "modify", "old_id": "8283b8ba2d98a978d7b51f8059c7c3a7ba01307b", "old_mode": 33188, "old_path": "src/Lean/Elab/Quotation.lean", "new_id": "0b9de00173b8f4f47967f138eb12f088c8412254", "new_mode": 33188, "new_path": "src/Lean/Elab/Quotation.lean" }, { "type": "modify", "old_id": "2ff261f1771e7d0a36c8cbc63e558d3c85136142", "old_mode": 33188, "old_path": "src/Lean/Elab/Tactic/BVDecide/LRAT/Trim.lean", "new_id": "c4c55373d6300d70cfc73a438eac2bc0ddf951d7", "new_mode": 33188, "new_path": "src/Lean/Elab/Tactic/BVDecide/LRAT/Trim.lean" }, { "type": "modify", "old_id": "0e1a4ce715eecaab330b28808ebbc23dbd8f7bc3", "old_mode": 33188, "old_path": "src/Lean/Elab/Tactic/Ext.lean", "new_id": "8b0b8e1762188343f11e147c3e027c215d23ff7b", "new_mode": 33188, "new_path": "src/Lean/Elab/Tactic/Ext.lean" }, { "type": "modify", "old_id": "1eb742eec14e523ffa230d4f4e669b380ee6484e", "old_mode": 33188, "old_path": "src/Lean/Elab/Tactic/Omega/Frontend.lean", "new_id": "bbfa147bb0ca5abcd0a978ab9681c96b18466ef2", "new_mode": 33188, "new_path": "src/Lean/Elab/Tactic/Omega/Frontend.lean" }, { "type": "modify", "old_id": "0a16656fd7a9d14367699d065d5def3348c2cd22", "old_mode": 33188, "old_path": "src/Lean/Environment.lean", "new_id": "5176b94df40f022fd19dc08aa869250b3535bdbb", "new_mode": 33188, "new_path": "src/Lean/Environment.lean" }, { "type": "modify", "old_id": "7d2ec3546acdd549fb4b1eea1da87b4a18fdf9e7", "old_mode": 33188, "old_path": "src/Lean/Expr.lean", "new_id": "2258c3cb1e56e8daa89034b9ce743c01199a6d98", "new_mode": 33188, "new_path": "src/Lean/Expr.lean" }, { "type": "modify", "old_id": "747978489fc37d87998955d294e5f40515d609a7", "old_mode": 33188, "old_path": "src/Lean/Linter/List.lean", "new_id": "49e6ff07bcb03e7078bdd1b4d53a507337c2ca16", "new_mode": 33188, "new_path": "src/Lean/Linter/List.lean" }, { "type": "modify", "old_id": "d8ac1de116f588f9879dde0be477255482517e9c", "old_mode": 33188, "old_path": "src/Lean/Meta/IndPredBelow.lean", "new_id": "2f8ad7bbf76bfa3c88e50627f6b7a7ca880bc07d", "new_mode": 33188, "new_path": "src/Lean/Meta/IndPredBelow.lean" }, { "type": "modify", "old_id": "946dc7e1c4735bb41769e6211c5921a4cb9f0b14", "old_mode": 33188, "old_path": "src/Lean/Meta/Match/MatcherApp/Basic.lean", "new_id": "5fb9fa0dd50518331160e04c91c779ccb987d648", "new_mode": 33188, "new_path": "src/Lean/Meta/Match/MatcherApp/Basic.lean" }, { "type": "modify", "old_id": "367d5a549cdd603c0e134cb738c0465a21b41b4a", "old_mode": 33188, "old_path": "src/Lean/Meta/SizeOf.lean", "new_id": "e4c458cd16f24a8a119176dd6333ffe1c7dadd12", "new_mode": 33188, "new_path": "src/Lean/Meta/SizeOf.lean" }, { "type": "modify", "old_id": "47e3349db690caa97dcf767300621dcf4ebd63a4", "old_mode": 33188, "old_path": "src/Lean/Meta/Tactic/FunInd.lean", "new_id": "24a917ba05fa233b8b490903fab460fc7620e9da", "new_mode": 33188, "new_path": "src/Lean/Meta/Tactic/FunInd.lean" }, { "type": "modify", "old_id": "6191cb6e31f80c4e3931b8bf93d96f4259fbc928", "old_mode": 33188, "old_path": "src/Lean/Meta/Tactic/Grind/Arith/Offset/Model.lean", "new_id": "9a2c1a8fa6b3252d84deb0ebcfbc9582f040e242", "new_mode": 33188, "new_path": "src/Lean/Meta/Tactic/Grind/Arith/Offset/Model.lean" }, { "type": "modify", "old_id": "9bc9478f0d8ed507c71f82f01994576585d0325a", "old_mode": 33188, "old_path": "src/Lean/Meta/Tactic/Grind/Ctor.lean", "new_id": "e9b8e79f53e42745eb83e4146b72792e27e898de", "new_mode": 33188, "new_path": "src/Lean/Meta/Tactic/Grind/Ctor.lean" }, { "type": "modify", "old_id": "9fe3ed891566703517ea9071e0cdac875c085563", "old_mode": 33188, "old_path": "src/Lean/Meta/Tactic/Grind/EMatch.lean", "new_id": "152c189eff29329bc64b694da8eeb6f750f114cd", "new_mode": 33188, "new_path": "src/Lean/Meta/Tactic/Grind/EMatch.lean" }, { "type": "modify", "old_id": "a0f458e0d80001333b29c5250e7d1240a046ff01", "old_mode": 33188, "old_path": "src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean", "new_id": "2d38450f330d85e718ea2a7ea6417edb677b8720", "new_mode": 33188, "new_path": "src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean" }, { "type": "modify", "old_id": "2bacc95fdc677324f642da9e2fbc1cc7bc4844a4", "old_mode": 33188, "old_path": "src/Lean/Syntax.lean", "new_id": "680e60acdc8804ee58a1228f6e00d7352d1c50d5", "new_mode": 33188, "new_path": "src/Lean/Syntax.lean" }, { "type": "modify", "old_id": "6208d40bf610a3d5a7dec0ecc55de4a0c4a54b4d", "old_mode": 33188, "old_path": "src/Lean/Util/ForEachExprWhere.lean", "new_id": "963e4baa33360583becf9555e913c608f78175f9", "new_mode": 33188, "new_path": "src/Lean/Util/ForEachExprWhere.lean" }, { "type": "modify", "old_id": "11d5881abc51697e12b25929a5d3d692c3d80d38", "old_mode": 33188, "old_path": "src/Lean/Util/ReplaceLevel.lean", "new_id": "007aa25d32100ffcb1c5284f262dd8ec0dcceccf", "new_mode": 33188, "new_path": "src/Lean/Util/ReplaceLevel.lean" }, { "type": "modify", "old_id": "07212ed0784a2fb2df37ea1d671c7a5ebf9f0985", "old_mode": 33188, "old_path": "src/Std/Data/DHashMap/Internal/Defs.lean", "new_id": "6f51f301b0a3855bedd7c312c562c13f6b957161", "new_mode": 33188, "new_path": "src/Std/Data/DHashMap/Internal/Defs.lean" }, { "type": "modify", "old_id": "86451719b2d8b5a17a52a94b442c4a07946763b6", "old_mode": 33188, "old_path": "src/Std/Data/DHashMap/Internal/Model.lean", "new_id": "6514e39961330cd37d3a63c4823b4407faf08a1e", "new_mode": 33188, "new_path": "src/Std/Data/DHashMap/Internal/Model.lean" }, { "type": "modify", "old_id": "023c96a2a7640f3588c9e02f25feef65c11b3c71", "old_mode": 33188, "old_path": "src/Std/Data/DHashMap/Internal/WF.lean", "new_id": "29f5d3afd36389833322bae76d044d9a1a9d908f", "new_mode": 33188, "new_path": "src/Std/Data/DHashMap/Internal/WF.lean" }, { "type": "modify", "old_id": "d1810717e22decea98650afef917cd1028d7e5c5", "old_mode": 33188, "old_path": "src/Std/Sat/AIG/CNF.lean", "new_id": "f4c114d5f1524e265aaf4e8409e48072dcab741c", "new_mode": 33188, "new_path": "src/Std/Sat/AIG/CNF.lean" }, { "type": "modify", "old_id": "d3f3c7b828a4c41b1ab0430716f8c8bf468c9a20", "old_mode": 33188, "old_path": "src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Implementation.lean", "new_id": "c545fcc870c2e7246a9f5902e0dc1e4f271d7631", "new_mode": 33188, "new_path": "src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Implementation.lean" }, { "type": "modify", "old_id": "9dbf71db48cfda0339b8de1e6a31e0b16d00cca5", "old_mode": 33188, "old_path": "src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean", "new_id": "710c7f455ae21dbe638b1970dd5114dd7688775a", "new_mode": 33188, "new_path": "src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean" } ] }