{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":760479517,"defaultBranch":"master","name":"lean4","ownerLogin":"opencompl","currentUserCanPush":false,"isFork":true,"isEmpty":false,"createdAt":"2024-02-20T13:55:12.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/76971994?v=4","public":true,"private":false,"isOrgOwned":true},"refInfo":{"name":"","listCacheKey":"v0:1726814177.0","currentOid":""},"activityList":{"items":[{"before":"69225c2ea87b6b797b0bd0c4b176fd5415d56892","after":"37b11eca32b2eb304ab86a26c9068de346e459bd","ref":"refs/heads/more_get_elem","pushedAt":"2024-09-20T06:56:04.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"tobiasgrosser","name":"Tobias Grosser","path":"/tobiasgrosser","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/521960?s=80&v=4"},"commit":{"message":"Fix test case","shortMessageHtmlLink":"Fix test case"}},{"before":"55df07b7b81c65be1b4addaedc16dc6cae4bab8f","after":"69225c2ea87b6b797b0bd0c4b176fd5415d56892","ref":"refs/heads/more_get_elem","pushedAt":"2024-09-20T06:36:57.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"tobiasgrosser","name":"Tobias Grosser","path":"/tobiasgrosser","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/521960?s=80&v=4"},"commit":{"message":"feat: more of BitVec.getElem_*","shortMessageHtmlLink":"feat: more of BitVec.getElem_*"}},{"before":null,"after":"55df07b7b81c65be1b4addaedc16dc6cae4bab8f","ref":"refs/heads/more_get_elem","pushedAt":"2024-09-20T06:36:17.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"tobiasgrosser","name":"Tobias Grosser","path":"/tobiasgrosser","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/521960?s=80&v=4"},"commit":{"message":"feat: more of BitVec.getELem_*","shortMessageHtmlLink":"feat: more of BitVec.getELem_*"}},{"before":null,"after":"165aa144f183edba68c059cf755b2cbb719b95ea","ref":"refs/heads/inhabited-tactic","pushedAt":"2024-09-20T03:17:46.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"alexkeizer","name":"Alex Keizer","path":"/alexkeizer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/18490187?s=80&v=4"},"commit":{"message":"feat: instance for `Inhabited (TacticM _)`","shortMessageHtmlLink":"feat: instance for <code>Inhabited (TacticM _)</code>"}},{"before":"3c53089d71a1b980b4485b991e4944a4d01bd8e9","after":"9720d28c5bd258b2b2123a7c253a9d3d9e3a0a63","ref":"refs/heads/getLsbD_getElem_simp","pushedAt":"2024-09-19T05:46:48.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"tobiasgrosser","name":"Tobias Grosser","path":"/tobiasgrosser","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/521960?s=80&v=4"},"commit":{"message":"WIP","shortMessageHtmlLink":"WIP"}},{"before":"fee34f865f9090f5b224caadeebf5a75d21e28b3","after":"3c53089d71a1b980b4485b991e4944a4d01bd8e9","ref":"refs/heads/getLsbD_getElem_simp","pushedAt":"2024-09-18T22:41:23.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"tobiasgrosser","name":"Tobias Grosser","path":"/tobiasgrosser","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/521960?s=80&v=4"},"commit":{"message":"Drop unused lemmas","shortMessageHtmlLink":"Drop unused lemmas"}},{"before":"708b8a7b02b85604ec7d5db15b6dd3696728ac18","after":"fee34f865f9090f5b224caadeebf5a75d21e28b3","ref":"refs/heads/getLsbD_getElem_simp","pushedAt":"2024-09-18T22:39:08.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"tobiasgrosser","name":"Tobias Grosser","path":"/tobiasgrosser","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/521960?s=80&v=4"},"commit":{"message":"WIP","shortMessageHtmlLink":"WIP"}},{"before":"fa6afa85df1c3d3e3a2fa8c7b4c417c0c86adb6e","after":"daf24ff6aab7fa1a43e97c5559d0eb71fe356aab","ref":"refs/heads/master","pushedAt":"2024-09-18T22:38:45.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"tobiasgrosser","name":"Tobias Grosser","path":"/tobiasgrosser","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/521960?s=80&v=4"},"commit":{"message":"feat: add BitVec.ofBool_[and|or|xor]_ofBool theorems (#5385)\n\n... and use them to simplify some proofs.","shortMessageHtmlLink":"feat: add BitVec.ofBool_[and|or|xor]_ofBool theorems (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2534584049\" data-permission-text=\"Title is private\" data-url=\"https://github.com/leanprover/lean4/issues/5385\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/leanprover/lean4/pull/5385/hovercard\" href=\"https://github.com/leanprover/lean4/pull/5385\">leanprover#5385</a>)"}},{"before":"2a5e1ae608fb35c1cf9d3beb4c7a0123f81e9c4d","after":"708b8a7b02b85604ec7d5db15b6dd3696728ac18","ref":"refs/heads/getLsbD_getElem_simp","pushedAt":"2024-09-18T22:38:23.000Z","pushType":"push","commitsCount":3,"pusher":{"login":"tobiasgrosser","name":"Tobias Grosser","path":"/tobiasgrosser","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/521960?s=80&v=4"},"commit":{"message":"Merge remote-tracking branch 'origin/master' into getLsbD_getElem_simp","shortMessageHtmlLink":"Merge remote-tracking branch 'origin/master' into getLsbD_getElem_simp"}},{"before":"f7f35ae24f69c24eb430ee824ff897c094e73525","after":"2a5e1ae608fb35c1cf9d3beb4c7a0123f81e9c4d","ref":"refs/heads/getLsbD_getElem_simp","pushedAt":"2024-09-18T21:40:56.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"tobiasgrosser","name":"Tobias Grosser","path":"/tobiasgrosser","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/521960?s=80&v=4"},"commit":{"message":"BitBlast","shortMessageHtmlLink":"BitBlast"}},{"before":"f626b7cf21e4eb3ab67a82a1c82c39ad19ad0329","after":"f7f35ae24f69c24eb430ee824ff897c094e73525","ref":"refs/heads/getLsbD_getElem_simp","pushedAt":"2024-09-18T21:26:59.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"tobiasgrosser","name":"Tobias Grosser","path":"/tobiasgrosser","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/521960?s=80&v=4"},"commit":{"message":"WIP","shortMessageHtmlLink":"WIP"}},{"before":"95b2a9cdd4a229f4b5fd6f9e95ebf94e3424c497","after":"0abf2391179059cc8a6b8f08fec5fd298fee7199","ref":"refs/heads/of_bool_and_or_xor","pushedAt":"2024-09-18T21:23:39.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"tobiasgrosser","name":"Tobias Grosser","path":"/tobiasgrosser","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/521960?s=80&v=4"},"commit":{"message":"Update tests/lean/interactive/completionPrv.lean.expected.out","shortMessageHtmlLink":"Update tests/lean/interactive/completionPrv.lean.expected.out"}},{"before":"3d734e6b191e0abcb41f20ffcd0bb50dc7a3ed65","after":"95b2a9cdd4a229f4b5fd6f9e95ebf94e3424c497","ref":"refs/heads/of_bool_and_or_xor","pushedAt":"2024-09-18T21:23:21.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"tobiasgrosser","name":"Tobias Grosser","path":"/tobiasgrosser","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/521960?s=80&v=4"},"commit":{"message":"Update tests/lean/interactive/completionPrv.lean.expected.out","shortMessageHtmlLink":"Update tests/lean/interactive/completionPrv.lean.expected.out"}},{"before":"7ac77c72f07aa655b085493d99ea437dec789ac7","after":"3d734e6b191e0abcb41f20ffcd0bb50dc7a3ed65","ref":"refs/heads/of_bool_and_or_xor","pushedAt":"2024-09-18T21:23:03.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"tobiasgrosser","name":"Tobias Grosser","path":"/tobiasgrosser","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/521960?s=80&v=4"},"commit":{"message":"Update tests/lean/interactive/completionPrv.lean.expected.out","shortMessageHtmlLink":"Update tests/lean/interactive/completionPrv.lean.expected.out"}},{"before":"521848a2ca8f1c903aa29380ba9075a3d08fde9e","after":"7ac77c72f07aa655b085493d99ea437dec789ac7","ref":"refs/heads/of_bool_and_or_xor","pushedAt":"2024-09-18T21:22:39.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"tobiasgrosser","name":"Tobias Grosser","path":"/tobiasgrosser","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/521960?s=80&v=4"},"commit":{"message":"Update tests/lean/interactive/completionPrv.lean.expected.out","shortMessageHtmlLink":"Update tests/lean/interactive/completionPrv.lean.expected.out"}},{"before":"52f4ca2160abe75a1ecde14d2c83aef0a11f250c","after":"521848a2ca8f1c903aa29380ba9075a3d08fde9e","ref":"refs/heads/of_bool_and_or_xor","pushedAt":"2024-09-18T21:21:58.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"tobiasgrosser","name":"Tobias Grosser","path":"/tobiasgrosser","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/521960?s=80&v=4"},"commit":{"message":"Update tests/lean/interactive/completionPrv.lean.expected.out","shortMessageHtmlLink":"Update tests/lean/interactive/completionPrv.lean.expected.out"}},{"before":"0182cf54644a46e0bbd84773c41b16a76bb0d0c8","after":"f626b7cf21e4eb3ab67a82a1c82c39ad19ad0329","ref":"refs/heads/getLsbD_getElem_simp","pushedAt":"2024-09-18T21:20:13.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"tobiasgrosser","name":"Tobias Grosser","path":"/tobiasgrosser","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/521960?s=80&v=4"},"commit":{"message":"GetELem bitblast","shortMessageHtmlLink":"GetELem bitblast"}},{"before":"909ad48eb1b1525c2072474565ddb71ef0f9661a","after":"52f4ca2160abe75a1ecde14d2c83aef0a11f250c","ref":"refs/heads/of_bool_and_or_xor","pushedAt":"2024-09-18T21:01:08.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"tobiasgrosser","name":"Tobias Grosser","path":"/tobiasgrosser","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/521960?s=80&v=4"},"commit":{"message":"Update src/Init/Data/BitVec/Lemmas.lean","shortMessageHtmlLink":"Update src/Init/Data/BitVec/Lemmas.lean"}},{"before":"013924653b06712ef72318bb445b83c8184ef9cf","after":"909ad48eb1b1525c2072474565ddb71ef0f9661a","ref":"refs/heads/of_bool_and_or_xor","pushedAt":"2024-09-18T20:51:17.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"tobiasgrosser","name":"Tobias Grosser","path":"/tobiasgrosser","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/521960?s=80&v=4"},"commit":{"message":"Fix test","shortMessageHtmlLink":"Fix test"}},{"before":"0c36ccfa4c65a3b28f6da07c621c0a1e38a816bb","after":"0182cf54644a46e0bbd84773c41b16a76bb0d0c8","ref":"refs/heads/getLsbD_getElem_simp","pushedAt":"2024-09-18T20:36:02.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"tobiasgrosser","name":"Tobias Grosser","path":"/tobiasgrosser","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/521960?s=80&v=4"},"commit":{"message":"Reduce diff","shortMessageHtmlLink":"Reduce diff"}},{"before":"f0ae45d6f71f8fa0877f7809e6fd46de84975575","after":"013924653b06712ef72318bb445b83c8184ef9cf","ref":"refs/heads/of_bool_and_or_xor","pushedAt":"2024-09-18T20:30:57.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"tobiasgrosser","name":"Tobias Grosser","path":"/tobiasgrosser","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/521960?s=80&v=4"},"commit":{"message":"Fix naming","shortMessageHtmlLink":"Fix naming"}},{"before":"598f860067e93dab8c7f5a880cd47926d1a8f8b1","after":"0c36ccfa4c65a3b28f6da07c621c0a1e38a816bb","ref":"refs/heads/getLsbD_getElem_simp","pushedAt":"2024-09-18T20:20:28.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"tobiasgrosser","name":"Tobias Grosser","path":"/tobiasgrosser","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/521960?s=80&v=4"},"commit":{"message":"Fix naming","shortMessageHtmlLink":"Fix naming"}},{"before":"699e427dda6a4c134f954652f6849fafd410d357","after":"598f860067e93dab8c7f5a880cd47926d1a8f8b1","ref":"refs/heads/getLsbD_getElem_simp","pushedAt":"2024-09-18T20:07:02.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"tobiasgrosser","name":"Tobias Grosser","path":"/tobiasgrosser","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/521960?s=80&v=4"},"commit":{"message":"WIP","shortMessageHtmlLink":"WIP"}},{"before":"dbde8fc0a891e6570468d02a618cfb9f88c57f34","after":"699e427dda6a4c134f954652f6849fafd410d357","ref":"refs/heads/getLsbD_getElem_simp","pushedAt":"2024-09-18T19:58:06.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"tobiasgrosser","name":"Tobias Grosser","path":"/tobiasgrosser","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/521960?s=80&v=4"},"commit":{"message":"WIP","shortMessageHtmlLink":"WIP"}},{"before":null,"after":"f0ae45d6f71f8fa0877f7809e6fd46de84975575","ref":"refs/heads/of_bool_and_or_xor","pushedAt":"2024-09-18T19:53:00.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"tobiasgrosser","name":"Tobias Grosser","path":"/tobiasgrosser","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/521960?s=80&v=4"},"commit":{"message":"feat: add BitVec.ofBool[and|or|xor] theorems\n\n... and use them to simplify some proofs.","shortMessageHtmlLink":"feat: add BitVec.ofBool[and|or|xor] theorems"}},{"before":"544e7df9f882bc372041518741464140abd96f83","after":"dbde8fc0a891e6570468d02a618cfb9f88c57f34","ref":"refs/heads/getLsbD_getElem_simp","pushedAt":"2024-09-18T19:32:03.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"tobiasgrosser","name":"Tobias Grosser","path":"/tobiasgrosser","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/521960?s=80&v=4"},"commit":{"message":"WIP","shortMessageHtmlLink":"WIP"}},{"before":"e379df00d097c5364fa8554a670c8467bd0c2ad2","after":"544e7df9f882bc372041518741464140abd96f83","ref":"refs/heads/getLsbD_getElem_simp","pushedAt":"2024-09-18T19:29:33.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"tobiasgrosser","name":"Tobias Grosser","path":"/tobiasgrosser","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/521960?s=80&v=4"},"commit":{"message":"WIP","shortMessageHtmlLink":"WIP"}},{"before":"f67d3365d45743fb4f64d3e98ba7da0354e91835","after":"e379df00d097c5364fa8554a670c8467bd0c2ad2","ref":"refs/heads/getLsbD_getElem_simp","pushedAt":"2024-09-18T19:10:21.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"tobiasgrosser","name":"Tobias Grosser","path":"/tobiasgrosser","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/521960?s=80&v=4"},"commit":{"message":"WIP","shortMessageHtmlLink":"WIP"}},{"before":"078e9b6d778932430adf9ecbbf02e1025e922ce1","after":"fa6afa85df1c3d3e3a2fa8c7b4c417c0c86adb6e","ref":"refs/heads/master","pushedAt":"2024-09-18T19:09:49.000Z","pushType":"push","commitsCount":22,"pusher":{"login":"tobiasgrosser","name":"Tobias Grosser","path":"/tobiasgrosser","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/521960?s=80&v=4"},"commit":{"message":"refactor: remove the last use of Lean.(HashSet|HashMap) (#5362)","shortMessageHtmlLink":"refactor: remove the last use of Lean.(HashSet|HashMap) (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2527911726\" data-permission-text=\"Title is private\" data-url=\"https://github.com/leanprover/lean4/issues/5362\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/leanprover/lean4/pull/5362/hovercard\" href=\"https://github.com/leanprover/lean4/pull/5362\">leanprover#5362</a>"}},{"before":"af7c12d56cb8047b03b5fe8032121723b0e32780","after":"f67d3365d45743fb4f64d3e98ba7da0354e91835","ref":"refs/heads/getLsbD_getElem_simp","pushedAt":"2024-09-18T19:08:37.000Z","pushType":"push","commitsCount":12,"pusher":{"login":"tobiasgrosser","name":"Tobias Grosser","path":"/tobiasgrosser","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/521960?s=80&v=4"},"commit":{"message":"WIP","shortMessageHtmlLink":"WIP"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"djE6ks8AAAAEu6QBjQA","startCursor":null,"endCursor":null}},"title":"Activity · opencompl/lean4"}