{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":638003982,"defaultBranch":"master","name":"GlimpseOfLean","ownerLogin":"PatrickMassot","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2023-05-08T22:01:10.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/14060883?v=4","public":true,"private":false,"isOrgOwned":false},"refInfo":{"name":"","listCacheKey":"v0:1683955980.758543","currentOid":""},"activityList":{"items":[{"before":"e8e9c6b6196dc82b758a08cd4f0051d25ec5c114","after":"8d73d32d90ec2315616ad8e720754eeacfb96af6","ref":"refs/heads/master","pushedAt":"2024-06-04T22:30:13.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"PatrickMassot","name":"Patrick Massot","path":"/PatrickMassot","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/14060883?s=80&v=4"},"commit":{"message":"Move lake configuration to toml","shortMessageHtmlLink":"Move lake configuration to toml"}},{"before":"fdf2c8eab05f92fbf98f441d65317768c15f6200","after":"e8e9c6b6196dc82b758a08cd4f0051d25ec5c114","ref":"refs/heads/master","pushedAt":"2023-09-25T13:56:50.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"PatrickMassot","name":"Patrick Massot","path":"/PatrickMassot","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/14060883?s=80&v=4"},"commit":{"message":"Bump Lean+Mathlib","shortMessageHtmlLink":"Bump Lean+Mathlib"}},{"before":"bf51c93ee3fd581cc3e380304417549d36748a35","after":"fdf2c8eab05f92fbf98f441d65317768c15f6200","ref":"refs/heads/master","pushedAt":"2023-07-08T18:51:39.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"PatrickMassot","name":"Patrick Massot","path":"/PatrickMassot","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/14060883?s=80&v=4"},"commit":{"message":"Update README.md","shortMessageHtmlLink":"Update README.md"}},{"before":"0a9c91793b2f632f29c8b5c738a5f404012fa033","after":"bf51c93ee3fd581cc3e380304417549d36748a35","ref":"refs/heads/master","pushedAt":"2023-07-08T18:50:54.000Z","pushType":"pr_merge","commitsCount":7,"pusher":{"login":"PatrickMassot","name":"Patrick Massot","path":"/PatrickMassot","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/14060883?s=80&v=4"},"commit":{"message":"Merge pull request #2 from fpvandoorn/LCchanges\n\nChanges from the Logic colloquium","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1795040011\" data-permission-text=\"Title is private\" data-url=\"https://github.com/PatrickMassot/GlimpseOfLean/issues/2\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/PatrickMassot/GlimpseOfLean/pull/2/hovercard\" href=\"https://github.com/PatrickMassot/GlimpseOfLean/pull/2\">#2</a> from fpvandoorn/LCchanges"}},{"before":"bf4b4f4de294acf5d446d9c8aa30131268389944","after":"0a9c91793b2f632f29c8b5c738a5f404012fa033","ref":"refs/heads/master","pushedAt":"2023-07-07T21:01:04.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"PatrickMassot","name":"Patrick Massot","path":"/PatrickMassot","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/14060883?s=80&v=4"},"commit":{"message":"Merge pull request #1 from jcommelin/patch-1\n\nFix two typos in Introduction.lean","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1745668070\" data-permission-text=\"Title is private\" data-url=\"https://github.com/PatrickMassot/GlimpseOfLean/issues/1\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/PatrickMassot/GlimpseOfLean/pull/1/hovercard\" href=\"https://github.com/PatrickMassot/GlimpseOfLean/pull/1\">#1</a> from jcommelin/patch-1"}},{"before":"0b140455ae36d3bb6e6caa6bd2dd615eb92620ad","after":"bf4b4f4de294acf5d446d9c8aa30131268389944","ref":"refs/heads/master","pushedAt":"2023-05-14T09:46:44.010Z","pushType":"push","commitsCount":1,"pusher":{"login":"PatrickMassot","name":"Patrick Massot","path":"/PatrickMassot","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/14060883?s=80&v=4"},"commit":{"message":"Delaborators for unions and intersections","shortMessageHtmlLink":"Delaborators for unions and intersections"}},{"before":"27a30d792e43a4ed07af4b7fed99b5b731fd229d","after":"0b140455ae36d3bb6e6caa6bd2dd615eb92620ad","ref":"refs/heads/master","pushedAt":"2023-05-13T09:10:20.788Z","pushType":"push","commitsCount":2,"pusher":{"login":"PatrickMassot","name":"Patrick Massot","path":"/PatrickMassot","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/14060883?s=80&v=4"},"commit":{"message":"Finish Galois solutions","shortMessageHtmlLink":"Finish Galois solutions"}},{"before":"4db75bdb377387305dda9f7dcab5522efb703329","after":null,"ref":"refs/heads/colloquium","pushedAt":"2023-05-13T05:33:00.758Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"PatrickMassot","name":"Patrick Massot","path":"/PatrickMassot","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/14060883?s=80&v=4"}},{"before":"577debf1383918b4957d47d29cf6f48932919b25","after":"27a30d792e43a4ed07af4b7fed99b5b731fd229d","ref":"refs/heads/master","pushedAt":"2023-05-12T13:01:53.457Z","pushType":"push","commitsCount":1,"pusher":{"login":"joneugster","name":"Jon Eugster","path":"/joneugster","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9141564?s=80&v=4"},"commit":{"message":"try to fix .gitpod.yml","shortMessageHtmlLink":"try to fix .gitpod.yml"}},{"before":"adb59a2fa8ab945fa0f1506d5dbf3debe37801ae","after":"577debf1383918b4957d47d29cf6f48932919b25","ref":"refs/heads/master","pushedAt":"2023-05-12T12:57:57.335Z","pushType":"push","commitsCount":1,"pusher":{"login":"joneugster","name":"Jon Eugster","path":"/joneugster","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/9141564?s=80&v=4"},"commit":{"message":"change .gitpod","shortMessageHtmlLink":"change .gitpod"}},{"before":"399f99d769b0eb522e112ce9e91455cd7b258f85","after":"adb59a2fa8ab945fa0f1506d5dbf3debe37801ae","ref":"refs/heads/master","pushedAt":"2023-05-12T12:54:55.701Z","pushType":"push","commitsCount":1,"pusher":{"login":"kmill","name":"Kyle Miller","path":"/kmill","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/235307?s=80&v=4"},"commit":{"message":"make pi notation not be scoped","shortMessageHtmlLink":"make pi notation not be scoped"}},{"before":"e0e8cc3b51bad595b3c8679fe1d92fd81743c6e1","after":"399f99d769b0eb522e112ce9e91455cd7b258f85","ref":"refs/heads/master","pushedAt":"2023-05-12T12:48:41.968Z","pushType":"push","commitsCount":1,"pusher":{"login":"kmill","name":"Kyle Miller","path":"/kmill","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/235307?s=80&v=4"},"commit":{"message":"fancy Exists delaborator","shortMessageHtmlLink":"fancy Exists delaborator"}},{"before":null,"after":"4db75bdb377387305dda9f7dcab5522efb703329","ref":"refs/heads/colloquium","pushedAt":"2023-05-12T12:33:05.899Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"PatrickMassot","name":"Patrick Massot","path":"/PatrickMassot","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/14060883?s=80&v=4"},"commit":{"message":"Colloquium files","shortMessageHtmlLink":"Colloquium files"}},{"before":"b4981aa1d44723c6ca2d8d9c525d2a406855a0ad","after":"e0e8cc3b51bad595b3c8679fe1d92fd81743c6e1","ref":"refs/heads/master","pushedAt":"2023-05-12T09:22:54.406Z","pushType":"push","commitsCount":1,"pusher":{"login":"kmill","name":"Kyle Miller","path":"/kmill","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/235307?s=80&v=4"},"commit":{"message":"improve docs to improve experience when hovering over\npi notation in infoview","shortMessageHtmlLink":"improve docs to improve experience when hovering over"}},{"before":"554a2b802b13b21d2520e2ede476871d64fbbd88","after":"b4981aa1d44723c6ca2d8d9c525d2a406855a0ad","ref":"refs/heads/master","pushedAt":"2023-05-12T08:58:02.243Z","pushType":"push","commitsCount":1,"pusher":{"login":"kmill","name":"Kyle Miller","path":"/kmill","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/235307?s=80&v=4"},"commit":{"message":"improve Prod.fst and Prod.snd with app unexpanders","shortMessageHtmlLink":"improve Prod.fst and Prod.snd with app unexpanders"}},{"before":"a96c6216532f3c641194c07e00d1e2f3c1627076","after":"554a2b802b13b21d2520e2ede476871d64fbbd88","ref":"refs/heads/master","pushedAt":"2023-05-11T21:39:09.872Z","pushType":"push","commitsCount":1,"pusher":{"login":"kmill","name":"Kyle Miller","path":"/kmill","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/235307?s=80&v=4"},"commit":{"message":"activate cute binders for inequalities","shortMessageHtmlLink":"activate cute binders for inequalities"}},{"before":"4445ea19f37fb31849a63860cfd4caa907faee13","after":"a96c6216532f3c641194c07e00d1e2f3c1627076","ref":"refs/heads/master","pushedAt":"2023-05-11T21:36:28.935Z","pushType":"push","commitsCount":1,"pusher":{"login":"kmill","name":"Kyle Miller","path":"/kmill","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/235307?s=80&v=4"},"commit":{"message":"unexpander for abs notation","shortMessageHtmlLink":"unexpander for abs notation"}},{"before":"1b0011511ac2711b7e4524985bd417b99a0e6a9f","after":"4445ea19f37fb31849a63860cfd4caa907faee13","ref":"refs/heads/master","pushedAt":"2023-05-11T21:33:49.717Z","pushType":"push","commitsCount":1,"pusher":{"login":"kmill","name":"Kyle Miller","path":"/kmill","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/235307?s=80&v=4"},"commit":{"message":"numeric projection notation for Prod.fst and Prod.snd","shortMessageHtmlLink":"numeric projection notation for Prod.fst and Prod.snd"}},{"before":"e968312749831b2623f66e23a879f134dad8417d","after":"1b0011511ac2711b7e4524985bd417b99a0e6a9f","ref":"refs/heads/master","pushedAt":"2023-05-11T12:41:15.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"PatrickMassot","name":"Patrick Massot","path":"/PatrickMassot","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/14060883?s=80&v=4"},"commit":{"message":"Add exercises about subgroups.","shortMessageHtmlLink":"Add exercises about subgroups."}},{"before":"eb799e68f721256fdbee77915fce96df59b2e101","after":"e968312749831b2623f66e23a879f134dad8417d","ref":"refs/heads/master","pushedAt":"2023-05-11T11:30:19.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"PatrickMassot","name":"Patrick Massot","path":"/PatrickMassot","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/14060883?s=80&v=4"},"commit":{"message":"Fix imports","shortMessageHtmlLink":"Fix imports"}},{"before":"0885cb31965c00c7ad5c104425d80352aa284bf7","after":"eb799e68f721256fdbee77915fce96df59b2e101","ref":"refs/heads/master","pushedAt":"2023-05-11T11:29:17.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"PatrickMassot","name":"Patrick Massot","path":"/PatrickMassot","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/14060883?s=80&v=4"},"commit":{"message":"Remove Chinese remainder from exercises","shortMessageHtmlLink":"Remove Chinese remainder from exercises"}},{"before":"b9b2f7b6aba6de3b05f0d310d8365a6b7bcfb795","after":"0885cb31965c00c7ad5c104425d80352aa284bf7","ref":"refs/heads/master","pushedAt":"2023-05-11T06:52:51.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"PatrickMassot","name":"Patrick Massot","path":"/PatrickMassot","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/14060883?s=80&v=4"},"commit":{"message":"Polish SequenceLimits","shortMessageHtmlLink":"Polish SequenceLimits"}},{"before":"17fc224e0a667d7cde4b8467c83e35de6d564e97","after":"b9b2f7b6aba6de3b05f0d310d8365a6b7bcfb795","ref":"refs/heads/master","pushedAt":"2023-05-11T06:05:51.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"PatrickMassot","name":"Patrick Massot","path":"/PatrickMassot","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/14060883?s=80&v=4"},"commit":{"message":"Update exercises files","shortMessageHtmlLink":"Update exercises files"}},{"before":"ed6e23bd878aad0577b99210480493200421dd7b","after":"17fc224e0a667d7cde4b8467c83e35de6d564e97","ref":"refs/heads/master","pushedAt":"2023-05-11T06:05:24.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"PatrickMassot","name":"Patrick Massot","path":"/PatrickMassot","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/14060883?s=80&v=4"},"commit":{"message":"Finish Galois file","shortMessageHtmlLink":"Finish Galois file"}},{"before":"cfbcd95a7a39708bd3d8c160dcd1351cee8ef5aa","after":"ed6e23bd878aad0577b99210480493200421dd7b","ref":"refs/heads/master","pushedAt":"2023-05-10T09:22:28.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"PatrickMassot","name":"Patrick Massot","path":"/PatrickMassot","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/14060883?s=80&v=4"},"commit":{"message":"Try to fix gitpod","shortMessageHtmlLink":"Try to fix gitpod"}},{"before":"e6f7500dd62b71b70d561633317d5cffaccd4823","after":"cfbcd95a7a39708bd3d8c160dcd1351cee8ef5aa","ref":"refs/heads/master","pushedAt":"2023-05-10T09:20:03.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"PatrickMassot","name":"Patrick Massot","path":"/PatrickMassot","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/14060883?s=80&v=4"},"commit":{"message":"Add GitPod link","shortMessageHtmlLink":"Add GitPod link"}},{"before":"c6824c16d08aa8e4668b81db0a6a7aa78d314fcf","after":"e6f7500dd62b71b70d561633317d5cffaccd4823","ref":"refs/heads/master","pushedAt":"2023-05-10T09:17:26.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"PatrickMassot","name":"Patrick Massot","path":"/PatrickMassot","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/14060883?s=80&v=4"},"commit":{"message":"Add VSCode settings","shortMessageHtmlLink":"Add VSCode settings"}},{"before":"54a16f596a1809cebb0143e665d5a7f5b7636195","after":"c6824c16d08aa8e4668b81db0a6a7aa78d314fcf","ref":"refs/heads/master","pushedAt":"2023-05-10T08:49:57.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"PatrickMassot","name":"Patrick Massot","path":"/PatrickMassot","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/14060883?s=80&v=4"},"commit":{"message":"Try adding cloud stuff","shortMessageHtmlLink":"Try adding cloud stuff"}},{"before":"e5a21def54996593dd04fb22e1a49fa3f3603739","after":"54a16f596a1809cebb0143e665d5a7f5b7636195","ref":"refs/heads/master","pushedAt":"2023-05-10T08:42:35.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"PatrickMassot","name":"Patrick Massot","path":"/PatrickMassot","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/14060883?s=80&v=4"},"commit":{"message":"Layout","shortMessageHtmlLink":"Layout"}},{"before":"28013bd2a58f42d34b6cc2300e580cc5e220ddb3","after":"e5a21def54996593dd04fb22e1a49fa3f3603739","ref":"refs/heads/master","pushedAt":"2023-05-10T08:39:02.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"PatrickMassot","name":"Patrick Massot","path":"/PatrickMassot","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/14060883?s=80&v=4"},"commit":{"message":"Make exercises files","shortMessageHtmlLink":"Make exercises files"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"djE6ks8AAAAEXIPHAwA","startCursor":null,"endCursor":null}},"title":"Activity · PatrickMassot/GlimpseOfLean"}