{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":596827147,"defaultBranch":"main","name":"McLTT","ownerLogin":"Beluga-lang","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2023-02-03T02:14:59.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/12446054?v=4","public":true,"private":false,"isOrgOwned":true},"refInfo":{"name":"","listCacheKey":"v0:1718265004.0","currentOid":""},"activityList":{"items":[{"before":"89e791077a72a9a91083cfa312871ddce06ffdb1","after":"b7abb3b69a06d2f9edad36b1920b7c6061fc69f7","ref":"refs/heads/pr-type-checker","pushedAt":"2024-06-13T11:59:34.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"Ailrun","name":"Junyoung/\"Clare\" Jang","path":"/Ailrun","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12473268?s=80&v=4"},"commit":{"message":"[WIP] type-checker problems","shortMessageHtmlLink":"[WIP] type-checker problems"}},{"before":"c45ad7083d000bdd4c4554497b5968349b880717","after":"89e791077a72a9a91083cfa312871ddce06ffdb1","ref":"refs/heads/pr-type-checker","pushedAt":"2024-06-13T11:27:10.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"Ailrun","name":"Junyoung/\"Clare\" Jang","path":"/Ailrun","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12473268?s=80&v=4"},"commit":{"message":"[WIP] type-checker problems","shortMessageHtmlLink":"[WIP] type-checker problems"}},{"before":"9d9c133695e49975daf458e519d7e3328b9c718e","after":"8c3dea4affff8a00112246f60c8fde0f25968d88","ref":"refs/heads/main","pushedAt":"2024-06-13T07:53:13.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"Ailrun","name":"Junyoung/\"Clare\" Jang","path":"/Ailrun","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12473268?s=80&v=4"},"commit":{"message":"Additional lemmas (#115)","shortMessageHtmlLink":"Additional lemmas (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2350426411\" data-permission-text=\"Title is private\" data-url=\"https://github.com/Beluga-lang/McLTT/issues/115\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/Beluga-lang/McLTT/pull/115/hovercard\" href=\"https://github.com/Beluga-lang/McLTT/pull/115\">#115</a>)"}},{"before":"20baa1efa86c92bf6baad1de4e190d17c3518e0d","after":"9d9c133695e49975daf458e519d7e3328b9c718e","ref":"refs/heads/main","pushedAt":"2024-06-13T07:52:41.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"Ailrun","name":"Junyoung/\"Clare\" Jang","path":"/Ailrun","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12473268?s=80&v=4"},"commit":{"message":"Update inversion theorems (#114)\n\n* Rename a constructor\r\n\r\n* Remove duplicated inversion theorems\r\n\r\n* Add an inversion theorem unexpectedly syntactic\r\n\r\n* Rearrange completeness consequences in a clearer structure","shortMessageHtmlLink":"Update inversion theorems (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2350424424\" data-permission-text=\"Title is private\" data-url=\"https://github.com/Beluga-lang/McLTT/issues/114\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/Beluga-lang/McLTT/pull/114/hovercard\" href=\"https://github.com/Beluga-lang/McLTT/pull/114\">#114</a>)"}},{"before":null,"after":"bf70507cc02d22b95778201ccaedc473f9bdd4e3","ref":"refs/heads/pr-additional-subsumption-lemmas","pushedAt":"2024-06-13T07:50:04.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"Ailrun","name":"Junyoung/\"Clare\" Jang","path":"/Ailrun","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12473268?s=80&v=4"},"commit":{"message":"Additional lemmas","shortMessageHtmlLink":"Additional lemmas"}},{"before":"a71f0ca2208f0680d531580eef1ed130b21bdd86","after":"1271e1918cb883e94d222e2cd9be6f3a1ce8fff5","ref":"refs/heads/pr-inversion-theorems","pushedAt":"2024-06-13T07:47:17.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"Ailrun","name":"Junyoung/\"Clare\" Jang","path":"/Ailrun","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12473268?s=80&v=4"},"commit":{"message":"Rearrange completeness consequences in a clearer structure","shortMessageHtmlLink":"Rearrange completeness consequences in a clearer structure"}},{"before":"18ce1837326fb5bff98a5691412b804f73ab497a","after":"20baa1efa86c92bf6baad1de4e190d17c3518e0d","ref":"refs/heads/main","pushedAt":"2024-06-13T01:18:10.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"Ailrun","name":"Junyoung/\"Clare\" Jang","path":"/Ailrun","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12473268?s=80&v=4"},"commit":{"message":"Add inversion theorems (#112)\n\n* Add inversion lemmas\r\n\r\n* Classify theorem as theorem","shortMessageHtmlLink":"Add inversion theorems (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2349586143\" data-permission-text=\"Title is private\" data-url=\"https://github.com/Beluga-lang/McLTT/issues/112\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/Beluga-lang/McLTT/pull/112/hovercard\" href=\"https://github.com/Beluga-lang/McLTT/pull/112\">#112</a>)"}},{"before":null,"after":"a71f0ca2208f0680d531580eef1ed130b21bdd86","ref":"refs/heads/pr-inversion-theorems","pushedAt":"2024-06-12T20:01:38.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"Ailrun","name":"Junyoung/\"Clare\" Jang","path":"/Ailrun","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12473268?s=80&v=4"},"commit":{"message":"Classify theorem as theorem","shortMessageHtmlLink":"Classify theorem as theorem"}},{"before":"80ee4953391b3a92bf354df30c842afe63e6bbbc","after":null,"ref":"refs/heads/pr-helper-lemmas","pushedAt":"2024-06-10T14:56:42.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"Ailrun","name":"Junyoung/\"Clare\" Jang","path":"/Ailrun","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12473268?s=80&v=4"}},{"before":"7a1777d18686eb4925ca1a84de77ab4eda9d661c","after":"18ce1837326fb5bff98a5691412b804f73ab497a","ref":"refs/heads/main","pushedAt":"2024-06-10T13:10:18.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"HuStmpHrrr","name":"Jason Hu","path":"/HuStmpHrrr","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/6101711?s=80&v=4"},"commit":{"message":"Add helper lemmas (#107)\n\n* Add optimized system\r\n\r\n* Update imports\r\n\r\n* Remove more premises","shortMessageHtmlLink":"Add helper lemmas (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2342105610\" data-permission-text=\"Title is private\" data-url=\"https://github.com/Beluga-lang/McLTT/issues/107\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/Beluga-lang/McLTT/pull/107/hovercard\" href=\"https://github.com/Beluga-lang/McLTT/pull/107\">#107</a>)"}},{"before":"3aced9f08ecb3c29c1d99972b615863c23b96fb4","after":"80ee4953391b3a92bf354df30c842afe63e6bbbc","ref":"refs/heads/pr-helper-lemmas","pushedAt":"2024-06-10T03:43:27.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Ailrun","name":"Junyoung/\"Clare\" Jang","path":"/Ailrun","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12473268?s=80&v=4"},"commit":{"message":"Remove more premises","shortMessageHtmlLink":"Remove more premises"}},{"before":"8d997aafd02af2692de738ec010dd6413361b418","after":"3aced9f08ecb3c29c1d99972b615863c23b96fb4","ref":"refs/heads/pr-helper-lemmas","pushedAt":"2024-06-09T08:42:48.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"Ailrun","name":"Junyoung/\"Clare\" Jang","path":"/Ailrun","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12473268?s=80&v=4"},"commit":{"message":"Update imports","shortMessageHtmlLink":"Update imports"}},{"before":null,"after":"8d997aafd02af2692de738ec010dd6413361b418","ref":"refs/heads/pr-helper-lemmas","pushedAt":"2024-06-09T08:40:21.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"Ailrun","name":"Junyoung/\"Clare\" Jang","path":"/Ailrun","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12473268?s=80&v=4"},"commit":{"message":"Update imports","shortMessageHtmlLink":"Update imports"}},{"before":"06a709bc4920b35d0811c3298b0996ac047162ec","after":"c45ad7083d000bdd4c4554497b5968349b880717","ref":"refs/heads/pr-type-checker","pushedAt":"2024-06-09T07:12:52.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"Ailrun","name":"Junyoung/\"Clare\" Jang","path":"/Ailrun","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12473268?s=80&v=4"},"commit":{"message":"[WIP] Implement type checker","shortMessageHtmlLink":"[WIP] Implement type checker"}},{"before":"fbac8600ac00e8290f57917894f7e026e2d60e79","after":null,"ref":"refs/heads/pr-conversion-and-cumulativity","pushedAt":"2024-06-09T00:46:18.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"Ailrun","name":"Junyoung/\"Clare\" Jang","path":"/Ailrun","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12473268?s=80&v=4"}},{"before":"cc2ed3c84be1b354501892d5a4404d08f159c67e","after":"7a1777d18686eb4925ca1a84de77ab4eda9d661c","ref":"refs/heads/main","pushedAt":"2024-06-09T00:46:14.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"Ailrun","name":"Junyoung/\"Clare\" Jang","path":"/Ailrun","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12473268?s=80&v=4"},"commit":{"message":"Add syntactic judgements for type subsumption (#101)\n\n* Add judgement for type subsumption\r\n\r\n* Add more lemmas\r\n\r\n* Try to impl subsumption checker\r\n\r\n* Resolve some comments\r\n\r\n* Move things a bit\r\n\r\n* Prove some more properties about subsumption\r\n\r\n* Define type subsumption decision algorithm\r\n\r\n* Make a tactic more stable\r\n\r\n* Remove Equations<question mark> command","shortMessageHtmlLink":"Add syntactic judgements for type subsumption (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2337180869\" data-permission-text=\"Title is private\" data-url=\"https://github.com/Beluga-lang/McLTT/issues/101\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/Beluga-lang/McLTT/pull/101/hovercard\" href=\"https://github.com/Beluga-lang/McLTT/pull/101\">#101</a>)"}},{"before":"07f490faa3543c35044adf19344aa9cc5553a11b","after":"fbac8600ac00e8290f57917894f7e026e2d60e79","ref":"refs/heads/pr-conversion-and-cumulativity","pushedAt":"2024-06-08T23:16:47.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Ailrun","name":"Junyoung/\"Clare\" Jang","path":"/Ailrun","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12473268?s=80&v=4"},"commit":{"message":"Remove Equations<question mark> command","shortMessageHtmlLink":"Remove Equations&lt;question mark&gt; command"}},{"before":"946bbff555595ee150032d5b3fb39e1639960159","after":"07f490faa3543c35044adf19344aa9cc5553a11b","ref":"refs/heads/pr-conversion-and-cumulativity","pushedAt":"2024-06-08T06:47:57.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Ailrun","name":"Junyoung/\"Clare\" Jang","path":"/Ailrun","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12473268?s=80&v=4"},"commit":{"message":"Make a tactic more stable","shortMessageHtmlLink":"Make a tactic more stable"}},{"before":"a493fabcf04bc192424c56ae11488370e3bd44a0","after":"946bbff555595ee150032d5b3fb39e1639960159","ref":"refs/heads/pr-conversion-and-cumulativity","pushedAt":"2024-06-08T06:45:21.000Z","pushType":"push","commitsCount":3,"pusher":{"login":"Ailrun","name":"Junyoung/\"Clare\" Jang","path":"/Ailrun","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12473268?s=80&v=4"},"commit":{"message":"Define type subsumption decision algorithm","shortMessageHtmlLink":"Define type subsumption decision algorithm"}},{"before":"1e4eb3a2d7000760a3ca2e2dd97c00918547881b","after":"a493fabcf04bc192424c56ae11488370e3bd44a0","ref":"refs/heads/pr-conversion-and-cumulativity","pushedAt":"2024-06-08T05:20:49.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Ailrun","name":"Junyoung/\"Clare\" Jang","path":"/Ailrun","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12473268?s=80&v=4"},"commit":{"message":"Resolve some comments","shortMessageHtmlLink":"Resolve some comments"}},{"before":"19837d024cae251293434e3164bc30386370ae68","after":null,"ref":"refs/heads/pr-update-actions","pushedAt":"2024-06-08T04:29:58.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"Ailrun","name":"Junyoung/\"Clare\" Jang","path":"/Ailrun","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12473268?s=80&v=4"}},{"before":"661892e606025fe49adb6f16c97f67c17e77cb15","after":"1e4eb3a2d7000760a3ca2e2dd97c00918547881b","ref":"refs/heads/pr-conversion-and-cumulativity","pushedAt":"2024-06-07T20:49:40.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"Ailrun","name":"Junyoung/\"Clare\" Jang","path":"/Ailrun","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12473268?s=80&v=4"},"commit":{"message":"Try to impl subsumption checker","shortMessageHtmlLink":"Try to impl subsumption checker"}},{"before":"215aa9595d54cc6cf658ea07778713b564e8eb7b","after":"661892e606025fe49adb6f16c97f67c17e77cb15","ref":"refs/heads/pr-conversion-and-cumulativity","pushedAt":"2024-06-07T09:20:25.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"Ailrun","name":"Junyoung/\"Clare\" Jang","path":"/Ailrun","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12473268?s=80&v=4"},"commit":{"message":"Add judgement for type subsumption","shortMessageHtmlLink":"Add judgement for type subsumption"}},{"before":"b46d026864e377dd04b007309d6a24a015187976","after":"cc2ed3c84be1b354501892d5a4404d08f159c67e","ref":"refs/heads/main","pushedAt":"2024-06-07T09:20:10.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"Ailrun","name":"Junyoung/\"Clare\" Jang","path":"/Ailrun","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12473268?s=80&v=4"},"commit":{"message":"Try container-based CI (#106)\n\n* Try container-based CI\r\n\r\n* Try fix CI\r\n\r\n* Update README accordingly\r\n\r\n* Update environment\r\n\r\n* Use the correct name\r\n\r\n* Fix permission issue\r\n\r\n* Remove pre-done part from CI\r\n\r\n* Update Dockerfile","shortMessageHtmlLink":"Try container-based CI (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2339626083\" data-permission-text=\"Title is private\" data-url=\"https://github.com/Beluga-lang/McLTT/issues/106\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/Beluga-lang/McLTT/pull/106/hovercard\" href=\"https://github.com/Beluga-lang/McLTT/pull/106\">#106</a>)"}},{"before":"3d17ad33337e27ac24a45a384039c7831744ad41","after":null,"ref":"refs/heads/pr-last-completeness-optimization","pushedAt":"2024-06-07T09:18:05.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"Ailrun","name":"Junyoung/\"Clare\" Jang","path":"/Ailrun","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12473268?s=80&v=4"}},{"before":"b464b61e21b7fdedf372ee9e40285e330e6443fc","after":"19837d024cae251293434e3164bc30386370ae68","ref":"refs/heads/pr-update-actions","pushedAt":"2024-06-07T09:17:07.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Ailrun","name":"Junyoung/\"Clare\" Jang","path":"/Ailrun","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12473268?s=80&v=4"},"commit":{"message":"Update Dockerfile","shortMessageHtmlLink":"Update Dockerfile"}},{"before":"cdb43b88dce53bc959b5bab98d000bd6ba3399b9","after":"b464b61e21b7fdedf372ee9e40285e330e6443fc","ref":"refs/heads/pr-update-actions","pushedAt":"2024-06-07T09:10:29.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"Ailrun","name":"Junyoung/\"Clare\" Jang","path":"/Ailrun","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12473268?s=80&v=4"},"commit":{"message":"Remove pre-done part from CI","shortMessageHtmlLink":"Remove pre-done part from CI"}},{"before":"d129fda8c7d7d68af45fef06d3bf70345e32a272","after":"cdb43b88dce53bc959b5bab98d000bd6ba3399b9","ref":"refs/heads/pr-update-actions","pushedAt":"2024-06-07T09:05:22.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"Ailrun","name":"Junyoung/\"Clare\" Jang","path":"/Ailrun","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12473268?s=80&v=4"},"commit":{"message":"Remove pre-done part from CI","shortMessageHtmlLink":"Remove pre-done part from CI"}},{"before":"2e45d2f5e587b17c572b649914ea993272b2b9b7","after":"d129fda8c7d7d68af45fef06d3bf70345e32a272","ref":"refs/heads/pr-update-actions","pushedAt":"2024-06-07T09:00:32.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"Ailrun","name":"Junyoung/\"Clare\" Jang","path":"/Ailrun","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12473268?s=80&v=4"},"commit":{"message":"Remove pre-done part from CI","shortMessageHtmlLink":"Remove pre-done part from CI"}},{"before":"908413d7bcf2da9b8e46d715bbe4675ec21a08b0","after":"2e45d2f5e587b17c572b649914ea993272b2b9b7","ref":"refs/heads/pr-update-actions","pushedAt":"2024-06-07T08:55:10.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"Ailrun","name":"Junyoung/\"Clare\" Jang","path":"/Ailrun","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/12473268?s=80&v=4"},"commit":{"message":"Remove pre-done part from CI","shortMessageHtmlLink":"Remove pre-done part from CI"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"djE6ks8AAAAEZFxktgA","startCursor":null,"endCursor":null}},"title":"Activity · Beluga-lang/McLTT"}