{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":129571436,"defaultBranch":"master","name":"lean4","ownerLogin":"leanprover","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2018-04-15T02:49:20.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/7233018?v=4","public":true,"private":false,"isOrgOwned":true},"refInfo":{"name":"","listCacheKey":"v0:1721772428.0","currentOid":""},"activityList":{"items":[{"before":null,"after":"dd7ec2de40dc150e3a983251a67b35eef7242b0d","ref":"refs/heads/joachim/ci-tweaks","pushedAt":"2024-07-23T22:07:08.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"nomeata","name":"Joachim Breitner","path":"/nomeata","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/148037?s=80&v=4"},"commit":{"message":"chore: ci: use check-stage3, not just build stage3\n\nto include the check that the stage2 and stage3 are identical. This was\nlost in #4032 it seems.","shortMessageHtmlLink":"chore: ci: use check-stage3, not just build stage3"}},{"before":"871c9b4164edc6ddcb148a7efb9f21fcd329b105","after":null,"ref":"refs/heads/gh-readonly-queue/master/pr-4815-ee6737ab4daf509be650be09d9c7852286078b6d","pushedAt":"2024-07-23T22:03:17.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"github-merge-queue[bot]","name":null,"path":"/apps/github-merge-queue","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9919?s=80&v=4"}},{"before":"ee6737ab4daf509be650be09d9c7852286078b6d","after":"871c9b4164edc6ddcb148a7efb9f21fcd329b105","ref":"refs/heads/master","pushedAt":"2024-07-23T22:03:16.000Z","pushType":"merge_queue_merge","commitsCount":1,"pusher":{"login":"github-merge-queue[bot]","name":null,"path":"/apps/github-merge-queue","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9919?s=80&v=4"},"commit":{"message":"test: update test output following stage0 update (#4815)\n\nthis is a consequenc of #4807 that only shows up once that change made\nit to stage0, it seem.","shortMessageHtmlLink":"test: update test output following stage0 update (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2426159773\" data-permission-text=\"Title is private\" data-url=\"https://github.com/leanprover/lean4/issues/4815\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/leanprover/lean4/pull/4815/hovercard\" href=\"https://github.com/leanprover/lean4/pull/4815\">#4815</a>)"}},{"before":null,"after":"871c9b4164edc6ddcb148a7efb9f21fcd329b105","ref":"refs/heads/gh-readonly-queue/master/pr-4815-ee6737ab4daf509be650be09d9c7852286078b6d","pushedAt":"2024-07-23T21:43:53.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"github-merge-queue[bot]","name":null,"path":"/apps/github-merge-queue","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9919?s=80&v=4"},"commit":{"message":"test: update test output following stage0 update (#4815)\n\nthis is a consequenc of #4807 that only shows up once that change made\nit to stage0, it seem.","shortMessageHtmlLink":"test: update test output following stage0 update (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2426159773\" data-permission-text=\"Title is private\" data-url=\"https://github.com/leanprover/lean4/issues/4815\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/leanprover/lean4/pull/4815/hovercard\" href=\"https://github.com/leanprover/lean4/pull/4815\">#4815</a>)"}},{"before":null,"after":"5d522c0a7bda28b85cb9cd1c91f1157af3ac7949","ref":"refs/heads/joachim/stage0-update-test-fixes","pushedAt":"2024-07-23T21:26:06.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"nomeata","name":"Joachim Breitner","path":"/nomeata","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/148037?s=80&v=4"},"commit":{"message":"test: update test output following stage0 update\n\nthis is a consequenc of #4807 that only shows up once that change made\nit to stage0, it seem.","shortMessageHtmlLink":"test: update test output following stage0 update"}},{"before":"7d60d8b5639170dc893b07841892493bf0475af6","after":"ee6737ab4daf509be650be09d9c7852286078b6d","ref":"refs/heads/master","pushedAt":"2024-07-23T16:15:04.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Kha","name":"Sebastian Ullrich","path":"/Kha","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/109126?s=80&v=4"},"commit":{"message":"chore: update stage0","shortMessageHtmlLink":"chore: update stage0"}},{"before":"7d60d8b5639170dc893b07841892493bf0475af6","after":null,"ref":"refs/heads/gh-readonly-queue/master/pr-4810-a4673e20a5151f680e3f07f6e5764b8a81cbc3cf","pushedAt":"2024-07-23T15:51:43.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"github-merge-queue[bot]","name":null,"path":"/apps/github-merge-queue","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9919?s=80&v=4"}},{"before":"a4673e20a5151f680e3f07f6e5764b8a81cbc3cf","after":"7d60d8b5639170dc893b07841892493bf0475af6","ref":"refs/heads/master","pushedAt":"2024-07-23T15:51:41.000Z","pushType":"merge_queue_merge","commitsCount":1,"pusher":{"login":"github-merge-queue[bot]","name":null,"path":"/apps/github-merge-queue","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9919?s=80&v=4"},"commit":{"message":"feat: safer #eval, and #eval! (#4810)\n\npreviously, `#eval` would happily evaluate expressions that contain\n`sorry`, either explicitly or because of failing tactics. In conjunction\nwith operations like array access this can lead to the lean process\ncrashing, which isn't particularly great.\n\nSo how `#eval` will refuse to run code that (transitively) depends on\nthe `sorry` axiom (using the same code as `#print axioms`).\n\nIf the user really wants to run it, they can use `#eval!`.\n\nCloses #1697","shortMessageHtmlLink":"feat: safer #eval, and #eval! (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2424621208\" data-permission-text=\"Title is private\" data-url=\"https://github.com/leanprover/lean4/issues/4810\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/leanprover/lean4/pull/4810/hovercard\" href=\"https://github.com/leanprover/lean4/pull/4810\">#4810</a>)"}},{"before":null,"after":"7d60d8b5639170dc893b07841892493bf0475af6","ref":"refs/heads/gh-readonly-queue/master/pr-4810-a4673e20a5151f680e3f07f6e5764b8a81cbc3cf","pushedAt":"2024-07-23T15:27:12.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"github-merge-queue[bot]","name":null,"path":"/apps/github-merge-queue","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9919?s=80&v=4"},"commit":{"message":"feat: safer #eval, and #eval! (#4810)\n\npreviously, `#eval` would happily evaluate expressions that contain\n`sorry`, either explicitly or because of failing tactics. In conjunction\nwith operations like array access this can lead to the lean process\ncrashing, which isn't particularly great.\n\nSo how `#eval` will refuse to run code that (transitively) depends on\nthe `sorry` axiom (using the same code as `#print axioms`).\n\nIf the user really wants to run it, they can use `#eval!`.\n\nCloses #1697","shortMessageHtmlLink":"feat: safer #eval, and #eval! (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2424621208\" data-permission-text=\"Title is private\" data-url=\"https://github.com/leanprover/lean4/issues/4810\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/leanprover/lean4/pull/4810/hovercard\" href=\"https://github.com/leanprover/lean4/pull/4810\">#4810</a>)"}},{"before":"22ae04f3e7ea716c4af5cfbab587370d10cc06fa","after":"5938dbbd14145c9b78f7645c4777f62a3fc8212c","ref":"refs/heads/nightly-with-mathlib","pushedAt":"2024-07-23T13:48:21.000Z","pushType":"push","commitsCount":6,"pusher":{"login":"leanprover-community-mathlib4-bot","name":null,"path":"/leanprover-community-mathlib4-bot","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/129911861?s=80&v=4"},"commit":{"message":"fix: make `elab_as_elim` eagerly elaborate arguments for parameters appearing in the types of targets (#4800)\n\nThe `elab_as_elim` elaborator eagerly elaborates arguments that can help\nwith elaborating the motive, however it does not include the transitive\nclosure of parameters appearing in types of parameters appearing in ...\ntypes of targets.\n\nThis leads to counter-intuitive behavior where arguments supplied to the\neliminator may unexpectedly have postponed elaboration, causing motives\nto be type incorrect for under-applied eliminators such as the\nfollowing:\n\n```lean\nclass IsEmpty (α : Sort u) : Prop where\n  protected false : α → False\n\n@[elab_as_elim]\ndef isEmptyElim [IsEmpty α] {p : α → Sort _} (a : α) : p a :=\n  (IsEmpty.false a).elim\n\nexample {α : Type _} [IsEmpty α] :\n  id (α → False) := isEmptyElim (α := α)\n```\n\nThe issue is that when `isEmptyElim (α := α)` is computing its motive,\nthe value of the postponed argument `α` is still an unassignable\nmetavariable. With this PR, this argument is now among those that are\neagerly elaborated since it appears as the type of the target `a`.\n\nThis PR also contains some other fixes:\n* When underapplied, does unification when instantiating foralls in the\nexpected type.\n* When overapplied, type checks the generalized-and-reverted expected\ntype.\n* When collecting targets, collects them in the correct order.\n\nAdds trace class `trace.Elab.app.elab_as_elim`.\n\nThis is a followup to #4722, which added motive type checking but\nexposed the eagerness issue.","shortMessageHtmlLink":"fix: make <code>elab_as_elim</code> eagerly elaborate arguments for parameters a…"}},{"before":"5bf8fb66927d2927f5d9b9dedfcdc5c5bd507cd2","after":null,"ref":"refs/heads/joachim/mutual-structural-notes","pushedAt":"2024-07-23T10:05:15.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"nomeata","name":"Joachim Breitner","path":"/nomeata","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/148037?s=80&v=4"}},{"before":"04f06eff4dad11800380c909b158a95571a242cd","after":"c60e916a1e9c63d560c72ef8e02e8c25751b2749","ref":"refs/heads/joachim/checkbang","pushedAt":"2024-07-23T10:04:29.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"nomeata","name":"Joachim Breitner","path":"/nomeata","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/148037?s=80&v=4"},"commit":{"message":"No bang after check","shortMessageHtmlLink":"No bang after check"}},{"before":"94816c8ea25ac63c0f36d54480697f2132e6e994","after":"04f06eff4dad11800380c909b158a95571a242cd","ref":"refs/heads/joachim/checkbang","pushedAt":"2024-07-23T09:45:19.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"nomeata","name":"Joachim Breitner","path":"/nomeata","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/148037?s=80&v=4"},"commit":{"message":"Need for stage0 update before tests","shortMessageHtmlLink":"Need for stage0 update before tests"}},{"before":"354a350f454bf1fd75559dab0f2038df306a7c21","after":"94816c8ea25ac63c0f36d54480697f2132e6e994","ref":"refs/heads/joachim/checkbang","pushedAt":"2024-07-23T09:25:16.000Z","pushType":"push","commitsCount":3,"pusher":{"login":"nomeata","name":"Joachim Breitner","path":"/nomeata","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/148037?s=80&v=4"},"commit":{"message":"Comment out a few #eval! in tests","shortMessageHtmlLink":"Comment out a few #eval! in tests"}},{"before":null,"after":"354a350f454bf1fd75559dab0f2038df306a7c21","ref":"refs/heads/joachim/checkbang","pushedAt":"2024-07-23T08:44:40.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"nomeata","name":"Joachim Breitner","path":"/nomeata","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/148037?s=80&v=4"},"commit":{"message":"feat: safer #eval, and #eval!\n\npreviously, `#eval` would happily evaluate expressions that contain\n`sorry`, either explicitly or because of failing tactics. In conjunction\nwith operations like array access this can lead to the lean process\ncrashing, which isn't particularly great.\n\nSo how `#eval` will refuse to run code that (transitively) depends on\nthe `sorry` axiom (using the same code as `#print axioms`).\n\nIf the user really wants to run it, they can use `#eval!`.","shortMessageHtmlLink":"feat: safer #eval, and #eval!"}},{"before":"22ae04f3e7ea716c4af5cfbab587370d10cc06fa","after":"5938dbbd14145c9b78f7645c4777f62a3fc8212c","ref":"refs/heads/nightly","pushedAt":"2024-07-23T08:14:10.000Z","pushType":"push","commitsCount":6,"pusher":{"login":"leodemoura","name":"Leonardo de Moura","path":"/leodemoura","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2778936?s=80&v=4"},"commit":{"message":"fix: make `elab_as_elim` eagerly elaborate arguments for parameters appearing in the types of targets (#4800)\n\nThe `elab_as_elim` elaborator eagerly elaborates arguments that can help\nwith elaborating the motive, however it does not include the transitive\nclosure of parameters appearing in types of parameters appearing in ...\ntypes of targets.\n\nThis leads to counter-intuitive behavior where arguments supplied to the\neliminator may unexpectedly have postponed elaboration, causing motives\nto be type incorrect for under-applied eliminators such as the\nfollowing:\n\n```lean\nclass IsEmpty (α : Sort u) : Prop where\n  protected false : α → False\n\n@[elab_as_elim]\ndef isEmptyElim [IsEmpty α] {p : α → Sort _} (a : α) : p a :=\n  (IsEmpty.false a).elim\n\nexample {α : Type _} [IsEmpty α] :\n  id (α → False) := isEmptyElim (α := α)\n```\n\nThe issue is that when `isEmptyElim (α := α)` is computing its motive,\nthe value of the postponed argument `α` is still an unassignable\nmetavariable. With this PR, this argument is now among those that are\neagerly elaborated since it appears as the type of the target `a`.\n\nThis PR also contains some other fixes:\n* When underapplied, does unification when instantiating foralls in the\nexpected type.\n* When overapplied, type checks the generalized-and-reverted expected\ntype.\n* When collecting targets, collects them in the correct order.\n\nAdds trace class `trace.Elab.app.elab_as_elim`.\n\nThis is a followup to #4722, which added motive type checking but\nexposed the eagerness issue.","shortMessageHtmlLink":"fix: make <code>elab_as_elim</code> eagerly elaborate arguments for parameters a…"}},{"before":"a4673e20a5151f680e3f07f6e5764b8a81cbc3cf","after":null,"ref":"refs/heads/gh-readonly-queue/master/pr-4808-b2ee8c240d4c45ec3ef2d6880c6595d7a8fe7b82","pushedAt":"2024-07-23T08:01:02.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"github-merge-queue[bot]","name":null,"path":"/apps/github-merge-queue","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9919?s=80&v=4"}},{"before":"b2ee8c240d4c45ec3ef2d6880c6595d7a8fe7b82","after":"a4673e20a5151f680e3f07f6e5764b8a81cbc3cf","ref":"refs/heads/master","pushedAt":"2024-07-23T08:01:01.000Z","pushType":"merge_queue_merge","commitsCount":1,"pusher":{"login":"github-merge-queue[bot]","name":null,"path":"/apps/github-merge-queue","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9919?s=80&v=4"},"commit":{"message":"chore: release notes for mutual structural induction (#4808)","shortMessageHtmlLink":"chore: release notes for mutual structural induction (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2423138583\" data-permission-text=\"Title is private\" data-url=\"https://github.com/leanprover/lean4/issues/4808\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/leanprover/lean4/pull/4808/hovercard\" href=\"https://github.com/leanprover/lean4/pull/4808\">#4808</a>)"}},{"before":"b2ee8c240d4c45ec3ef2d6880c6595d7a8fe7b82","after":null,"ref":"refs/heads/gh-readonly-queue/master/pr-4806-5d632a97b838b0e701006903c51edc94aa579007","pushedAt":"2024-07-23T07:53:16.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"github-merge-queue[bot]","name":null,"path":"/apps/github-merge-queue","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9919?s=80&v=4"}},{"before":"5d632a97b838b0e701006903c51edc94aa579007","after":"b2ee8c240d4c45ec3ef2d6880c6595d7a8fe7b82","ref":"refs/heads/master","pushedAt":"2024-07-23T07:53:15.000Z","pushType":"merge_queue_merge","commitsCount":1,"pusher":{"login":"github-merge-queue[bot]","name":null,"path":"/apps/github-merge-queue","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9919?s=80&v=4"},"commit":{"message":"doc: update quickstart guide (#4806)\n\nThis PR updates the screenshots and instructions in the quickstart guide\nfor the most recent Lean 4 VS Code extension version and makes a small\nstylistic change suggested by @semorrison.","shortMessageHtmlLink":"doc: update quickstart guide (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2422408355\" data-permission-text=\"Title is private\" data-url=\"https://github.com/leanprover/lean4/issues/4806\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/leanprover/lean4/pull/4806/hovercard\" href=\"https://github.com/leanprover/lean4/pull/4806\">#4806</a>)"}},{"before":null,"after":"a4673e20a5151f680e3f07f6e5764b8a81cbc3cf","ref":"refs/heads/gh-readonly-queue/master/pr-4808-b2ee8c240d4c45ec3ef2d6880c6595d7a8fe7b82","pushedAt":"2024-07-23T07:40:45.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"github-merge-queue[bot]","name":null,"path":"/apps/github-merge-queue","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9919?s=80&v=4"},"commit":{"message":"chore: release notes for mutual structural induction (#4808)","shortMessageHtmlLink":"chore: release notes for mutual structural induction (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2423138583\" data-permission-text=\"Title is private\" data-url=\"https://github.com/leanprover/lean4/issues/4808\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/leanprover/lean4/pull/4808/hovercard\" href=\"https://github.com/leanprover/lean4/pull/4808\">#4808</a>)"}},{"before":null,"after":"b2ee8c240d4c45ec3ef2d6880c6595d7a8fe7b82","ref":"refs/heads/gh-readonly-queue/master/pr-4806-5d632a97b838b0e701006903c51edc94aa579007","pushedAt":"2024-07-23T07:31:36.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"github-merge-queue[bot]","name":null,"path":"/apps/github-merge-queue","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9919?s=80&v=4"},"commit":{"message":"doc: update quickstart guide (#4806)\n\nThis PR updates the screenshots and instructions in the quickstart guide\nfor the most recent Lean 4 VS Code extension version and makes a small\nstylistic change suggested by @semorrison.","shortMessageHtmlLink":"doc: update quickstart guide (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2422408355\" data-permission-text=\"Title is private\" data-url=\"https://github.com/leanprover/lean4/issues/4806\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/leanprover/lean4/pull/4806/hovercard\" href=\"https://github.com/leanprover/lean4/pull/4806\">#4806</a>)"}},{"before":"5d632a97b838b0e701006903c51edc94aa579007","after":null,"ref":"refs/heads/gh-readonly-queue/master/pr-4803-5938dbbd14145c9b78f7645c4777f62a3fc8212c","pushedAt":"2024-07-23T07:18:30.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"github-merge-queue[bot]","name":null,"path":"/apps/github-merge-queue","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9919?s=80&v=4"}},{"before":"5938dbbd14145c9b78f7645c4777f62a3fc8212c","after":"5d632a97b838b0e701006903c51edc94aa579007","ref":"refs/heads/master","pushedAt":"2024-07-23T07:18:29.000Z","pushType":"merge_queue_merge","commitsCount":1,"pusher":{"login":"github-merge-queue[bot]","name":null,"path":"/apps/github-merge-queue","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9919?s=80&v=4"},"commit":{"message":"feat: more hash map lemmas (#4803)","shortMessageHtmlLink":"feat: more hash map lemmas (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2421372293\" data-permission-text=\"Title is private\" data-url=\"https://github.com/leanprover/lean4/issues/4803\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/leanprover/lean4/pull/4803/hovercard\" href=\"https://github.com/leanprover/lean4/pull/4803\">#4803</a>)"}},{"before":null,"after":"5d632a97b838b0e701006903c51edc94aa579007","ref":"refs/heads/gh-readonly-queue/master/pr-4803-5938dbbd14145c9b78f7645c4777f62a3fc8212c","pushedAt":"2024-07-23T06:57:59.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"github-merge-queue[bot]","name":null,"path":"/apps/github-merge-queue","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9919?s=80&v=4"},"commit":{"message":"feat: more hash map lemmas (#4803)","shortMessageHtmlLink":"feat: more hash map lemmas (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2421372293\" data-permission-text=\"Title is private\" data-url=\"https://github.com/leanprover/lean4/issues/4803\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/leanprover/lean4/pull/4803/hovercard\" href=\"https://github.com/leanprover/lean4/pull/4803\">#4803</a>)"}},{"before":"d48198d9a995882eab0f1d6e58773060c54f3721","after":"f427340932cd3a5cb1f07ee469524b847d50f00d","ref":"refs/heads/markus/hashmap-more-lemmas","pushedAt":"2024-07-23T06:43:32.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"TwoFX","name":"Markus Himmel","path":"/TwoFX","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2065352?s=80&v=4"},"commit":{"message":"feat: more hash map lemmas","shortMessageHtmlLink":"feat: more hash map lemmas"}},{"before":"5938dbbd14145c9b78f7645c4777f62a3fc8212c","after":null,"ref":"refs/heads/gh-readonly-queue/master/pr-4800-852add3e55ed8c94bc496f35019674f046ab0d5e","pushedAt":"2024-07-22T23:46:06.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"github-merge-queue[bot]","name":null,"path":"/apps/github-merge-queue","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9919?s=80&v=4"}},{"before":"852add3e55ed8c94bc496f35019674f046ab0d5e","after":"5938dbbd14145c9b78f7645c4777f62a3fc8212c","ref":"refs/heads/master","pushedAt":"2024-07-22T23:46:05.000Z","pushType":"merge_queue_merge","commitsCount":1,"pusher":{"login":"github-merge-queue[bot]","name":null,"path":"/apps/github-merge-queue","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9919?s=80&v=4"},"commit":{"message":"fix: make `elab_as_elim` eagerly elaborate arguments for parameters appearing in the types of targets (#4800)\n\nThe `elab_as_elim` elaborator eagerly elaborates arguments that can help\nwith elaborating the motive, however it does not include the transitive\nclosure of parameters appearing in types of parameters appearing in ...\ntypes of targets.\n\nThis leads to counter-intuitive behavior where arguments supplied to the\neliminator may unexpectedly have postponed elaboration, causing motives\nto be type incorrect for under-applied eliminators such as the\nfollowing:\n\n```lean\nclass IsEmpty (α : Sort u) : Prop where\n  protected false : α → False\n\n@[elab_as_elim]\ndef isEmptyElim [IsEmpty α] {p : α → Sort _} (a : α) : p a :=\n  (IsEmpty.false a).elim\n\nexample {α : Type _} [IsEmpty α] :\n  id (α → False) := isEmptyElim (α := α)\n```\n\nThe issue is that when `isEmptyElim (α := α)` is computing its motive,\nthe value of the postponed argument `α` is still an unassignable\nmetavariable. With this PR, this argument is now among those that are\neagerly elaborated since it appears as the type of the target `a`.\n\nThis PR also contains some other fixes:\n* When underapplied, does unification when instantiating foralls in the\nexpected type.\n* When overapplied, type checks the generalized-and-reverted expected\ntype.\n* When collecting targets, collects them in the correct order.\n\nAdds trace class `trace.Elab.app.elab_as_elim`.\n\nThis is a followup to #4722, which added motive type checking but\nexposed the eagerness issue.","shortMessageHtmlLink":"fix: make <code>elab_as_elim</code> eagerly elaborate arguments for parameters a…"}},{"before":null,"after":"5938dbbd14145c9b78f7645c4777f62a3fc8212c","ref":"refs/heads/gh-readonly-queue/master/pr-4800-852add3e55ed8c94bc496f35019674f046ab0d5e","pushedAt":"2024-07-22T23:23:45.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"github-merge-queue[bot]","name":null,"path":"/apps/github-merge-queue","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9919?s=80&v=4"},"commit":{"message":"fix: make `elab_as_elim` eagerly elaborate arguments for parameters appearing in the types of targets (#4800)\n\nThe `elab_as_elim` elaborator eagerly elaborates arguments that can help\nwith elaborating the motive, however it does not include the transitive\nclosure of parameters appearing in types of parameters appearing in ...\ntypes of targets.\n\nThis leads to counter-intuitive behavior where arguments supplied to the\neliminator may unexpectedly have postponed elaboration, causing motives\nto be type incorrect for under-applied eliminators such as the\nfollowing:\n\n```lean\nclass IsEmpty (α : Sort u) : Prop where\n  protected false : α → False\n\n@[elab_as_elim]\ndef isEmptyElim [IsEmpty α] {p : α → Sort _} (a : α) : p a :=\n  (IsEmpty.false a).elim\n\nexample {α : Type _} [IsEmpty α] :\n  id (α → False) := isEmptyElim (α := α)\n```\n\nThe issue is that when `isEmptyElim (α := α)` is computing its motive,\nthe value of the postponed argument `α` is still an unassignable\nmetavariable. With this PR, this argument is now among those that are\neagerly elaborated since it appears as the type of the target `a`.\n\nThis PR also contains some other fixes:\n* When underapplied, does unification when instantiating foralls in the\nexpected type.\n* When overapplied, type checks the generalized-and-reverted expected\ntype.\n* When collecting targets, collects them in the correct order.\n\nAdds trace class `trace.Elab.app.elab_as_elim`.\n\nThis is a followup to #4722, which added motive type checking but\nexposed the eagerness issue.","shortMessageHtmlLink":"fix: make <code>elab_as_elim</code> eagerly elaborate arguments for parameters a…"}},{"before":"852add3e55ed8c94bc496f35019674f046ab0d5e","after":null,"ref":"refs/heads/gh-readonly-queue/master/pr-4748-20c857147c2496a806b3390012f99e08dfaa1741","pushedAt":"2024-07-22T22:17:38.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"github-merge-queue[bot]","name":null,"path":"/apps/github-merge-queue","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9919?s=80&v=4"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"djE6ks8AAAAEh1TDDQA","startCursor":null,"endCursor":null}},"title":"Activity · leanprover/lean4"}