{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":422605067,"defaultBranch":"main","name":"proofs","ownerLogin":"katydid","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2021-10-29T14:26:24.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/9207606?v=4","public":true,"private":false,"isOrgOwned":true},"refInfo":{"name":"","listCacheKey":"v0:1710515408.0","currentOid":""},"activityList":{"items":[{"before":"aa171da88bdcde710adadf7c473c438f30e7dcd8","after":null,"ref":"refs/heads/decidable","pushedAt":"2024-03-15T15:10:08.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"awalterschulze","name":"Walter Schulze","path":"/awalterschulze","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1829933?s=80&v=4"}},{"before":"0002f111f94d53f9ebdc769a31c3a2f4388f2aa6","after":"8105af686a3bdf193909567f5165835001240640","ref":"refs/heads/main","pushedAt":"2024-03-15T15:10:05.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"awalterschulze","name":"Walter Schulze","path":"/awalterschulze","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1829933?s=80&v=4"},"commit":{"message":"Lang and dLang","shortMessageHtmlLink":"Lang and dLang"}},{"before":null,"after":"aa171da88bdcde710adadf7c473c438f30e7dcd8","ref":"refs/heads/decidable","pushedAt":"2024-03-15T14:58:04.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"awalterschulze","name":"Walter Schulze","path":"/awalterschulze","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1829933?s=80&v=4"},"commit":{"message":"Lang and dLang","shortMessageHtmlLink":"Lang and dLang"}},{"before":"97aa8604df25dc09c5efbca0b13b331af1cc6a2c","after":null,"ref":"refs/heads/trfl","pushedAt":"2024-02-25T15:46:44.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"awalterschulze","name":"Walter Schulze","path":"/awalterschulze","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1829933?s=80&v=4"}},{"before":"612d709960dca637aa93f26da9430cf096f85d71","after":"0002f111f94d53f9ebdc769a31c3a2f4388f2aa6","ref":"refs/heads/main","pushedAt":"2024-02-25T15:46:41.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"awalterschulze","name":"Walter Schulze","path":"/awalterschulze","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1829933?s=80&v=4"},"commit":{"message":"trfl function","shortMessageHtmlLink":"trfl function"}},{"before":null,"after":"97aa8604df25dc09c5efbca0b13b331af1cc6a2c","ref":"refs/heads/trfl","pushedAt":"2024-02-25T15:37:47.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"awalterschulze","name":"Walter Schulze","path":"/awalterschulze","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1829933?s=80&v=4"},"commit":{"message":"trfl function","shortMessageHtmlLink":"trfl function"}},{"before":"1f7745d8369b4e33f937dc2c57057fa69fa45162","after":null,"ref":"refs/heads/lean4.5","pushedAt":"2024-02-25T15:01:50.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"awalterschulze","name":"Walter Schulze","path":"/awalterschulze","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1829933?s=80&v=4"}},{"before":"ad2be0ffe70def214ee001a6f62d95b47f2b33d7","after":"612d709960dca637aa93f26da9430cf096f85d71","ref":"refs/heads/main","pushedAt":"2024-02-25T15:01:47.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"awalterschulze","name":"Walter Schulze","path":"/awalterschulze","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1829933?s=80&v=4"},"commit":{"message":"Update Lean version","shortMessageHtmlLink":"Update Lean version"}},{"before":null,"after":"1f7745d8369b4e33f937dc2c57057fa69fa45162","ref":"refs/heads/lean4.5","pushedAt":"2024-02-25T14:47:11.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"awalterschulze","name":"Walter Schulze","path":"/awalterschulze","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1829933?s=80&v=4"},"commit":{"message":"Update Lean version","shortMessageHtmlLink":"Update Lean version"}},{"before":"130763e13407e898f543f419c69b9b4328ed7375","after":null,"ref":"refs/heads/proof_revelant_parse","pushedAt":"2024-02-03T18:10:21.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"awalterschulze","name":"Walter Schulze","path":"/awalterschulze","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1829933?s=80&v=4"}},{"before":"a9f7918b3498eea5a9abd74ab374172b3caab5a3","after":"ad2be0ffe70def214ee001a6f62d95b47f2b33d7","ref":"refs/heads/main","pushedAt":"2024-02-03T18:10:18.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"awalterschulze","name":"Walter Schulze","path":"/awalterschulze","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1829933?s=80&v=4"},"commit":{"message":"proof relevant parse 2","shortMessageHtmlLink":"proof relevant parse 2"}},{"before":null,"after":"130763e13407e898f543f419c69b9b4328ed7375","ref":"refs/heads/proof_revelant_parse","pushedAt":"2024-02-03T18:02:53.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"awalterschulze","name":"Walter Schulze","path":"/awalterschulze","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1829933?s=80&v=4"},"commit":{"message":"proof relevant parse 2","shortMessageHtmlLink":"proof relevant parse 2"}},{"before":"b5a067a1ed95d1e09ed5017c0bac158066ba5781","after":null,"ref":"refs/heads/cleanup","pushedAt":"2024-02-03T17:51:30.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"awalterschulze","name":"Walter Schulze","path":"/awalterschulze","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1829933?s=80&v=4"}},{"before":"4150dbf12ba21c7dc1e9f702b72875ba301c1e6a","after":"a9f7918b3498eea5a9abd74ab374172b3caab5a3","ref":"refs/heads/main","pushedAt":"2024-02-03T17:51:27.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"awalterschulze","name":"Walter Schulze","path":"/awalterschulze","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1829933?s=80&v=4"},"commit":{"message":"massive cleanup\n\nDelete Hott\nDelete RegexNotation\nDelete TDecidable","shortMessageHtmlLink":"massive cleanup"}},{"before":null,"after":"b5a067a1ed95d1e09ed5017c0bac158066ba5781","ref":"refs/heads/cleanup","pushedAt":"2024-02-03T17:39:53.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"awalterschulze","name":"Walter Schulze","path":"/awalterschulze","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1829933?s=80&v=4"},"commit":{"message":"massive cleanup\n\nDelete Hott\nDelete RegexNotation\nDelete TDecidable","shortMessageHtmlLink":"massive cleanup"}},{"before":"6d11a98265bf5d3bdb4537b75435ff30772b08ef","after":"4150dbf12ba21c7dc1e9f702b72875ba301c1e6a","ref":"refs/heads/main","pushedAt":"2024-02-03T15:15:15.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"awalterschulze","name":"Walter Schulze","path":"/awalterschulze","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1829933?s=80&v=4"},"commit":{"message":"Try out Homotopy Type Theory","shortMessageHtmlLink":"Try out Homotopy Type Theory"}},{"before":null,"after":"e64b201052635bc25d2635f67a3dab3bc0cf188e","ref":"refs/heads/tryhott","pushedAt":"2024-02-03T15:12:50.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"awalterschulze","name":"Walter Schulze","path":"/awalterschulze","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1829933?s=80&v=4"},"commit":{"message":"Try out Homotopy Type Theory","shortMessageHtmlLink":"Try out Homotopy Type Theory"}},{"before":"4effa43d57f4cf0fdcae87f6ecbd2034ebd12af0","after":null,"ref":"refs/heads/hott","pushedAt":"2024-01-28T13:07:16.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"awalterschulze","name":"Walter Schulze","path":"/awalterschulze","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1829933?s=80&v=4"}},{"before":"a5256b193d16f4086e2c20bd33cec5b205952546","after":"6d11a98265bf5d3bdb4537b75435ff30772b08ef","ref":"refs/heads/main","pushedAt":"2024-01-28T13:07:14.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"awalterschulze","name":"Walter Schulze","path":"/awalterschulze","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1829933?s=80&v=4"},"commit":{"message":"Hott alternatives for Language and Calculus","shortMessageHtmlLink":"Hott alternatives for Language and Calculus"}},{"before":null,"after":"4effa43d57f4cf0fdcae87f6ecbd2034ebd12af0","ref":"refs/heads/hott","pushedAt":"2024-01-28T13:04:36.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"awalterschulze","name":"Walter Schulze","path":"/awalterschulze","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1829933?s=80&v=4"},"commit":{"message":"Hott alternatives for Language and Calculus","shortMessageHtmlLink":"Hott alternatives for Language and Calculus"}},{"before":"77df7c5a9bb218f7c6aea832d22e304844ebb4d4","after":null,"ref":"refs/heads/groundzero","pushedAt":"2024-01-28T12:14:44.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"awalterschulze","name":"Walter Schulze","path":"/awalterschulze","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1829933?s=80&v=4"}},{"before":"e355e8b469317e6767ba43ec0c0efea8fdb1d6a1","after":"a5256b193d16f4086e2c20bd33cec5b205952546","ref":"refs/heads/main","pushedAt":"2024-01-28T12:14:42.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"awalterschulze","name":"Walter Schulze","path":"/awalterschulze","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1829933?s=80&v=4"},"commit":{"message":"Add groundzero dependency and update lean-toolchain","shortMessageHtmlLink":"Add groundzero dependency and update lean-toolchain"}},{"before":null,"after":"77df7c5a9bb218f7c6aea832d22e304844ebb4d4","ref":"refs/heads/groundzero","pushedAt":"2024-01-28T12:07:31.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"awalterschulze","name":"Walter Schulze","path":"/awalterschulze","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1829933?s=80&v=4"},"commit":{"message":"Add groundzero dependency and update lean-toolchain","shortMessageHtmlLink":"Add groundzero dependency and update lean-toolchain"}},{"before":"10718235fb9584fa911a8546661cf14922a77c34","after":null,"ref":"refs/heads/allotherthingsbeingequal","pushedAt":"2024-01-28T12:03:04.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"awalterschulze","name":"Walter Schulze","path":"/awalterschulze","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1829933?s=80&v=4"}},{"before":"93af2adcd8a0a25491af5c6a22e3f36f2402cfb6","after":"e355e8b469317e6767ba43ec0c0efea8fdb1d6a1","ref":"refs/heads/main","pushedAt":"2024-01-28T12:03:02.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"awalterschulze","name":"Walter Schulze","path":"/awalterschulze","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1829933?s=80&v=4"},"commit":{"message":"some surprising proofs about Eq and TEq","shortMessageHtmlLink":"some surprising proofs about Eq and TEq"}},{"before":null,"after":"10718235fb9584fa911a8546661cf14922a77c34","ref":"refs/heads/allotherthingsbeingequal","pushedAt":"2024-01-28T11:56:09.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"awalterschulze","name":"Walter Schulze","path":"/awalterschulze","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1829933?s=80&v=4"},"commit":{"message":"some surprising proofs about Eq and TEq","shortMessageHtmlLink":"some surprising proofs about Eq and TEq"}},{"before":"4f338ca1fcdce7e03ea8dd5f066922b3e4aeb830","after":null,"ref":"refs/heads/some_confusion","pushedAt":"2024-01-21T17:24:09.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"awalterschulze","name":"Walter Schulze","path":"/awalterschulze","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1829933?s=80&v=4"}},{"before":"9a433def6e1760dc80bc929935efe2a26320a8ab","after":"93af2adcd8a0a25491af5c6a22e3f36f2402cfb6","ref":"refs/heads/main","pushedAt":"2024-01-21T17:24:06.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"awalterschulze","name":"Walter Schulze","path":"/awalterschulze","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1829933?s=80&v=4"},"commit":{"message":"TEq = Eq\n\nIt is now possible to go between TEq and Eq\nNat is now TDecidable","shortMessageHtmlLink":"TEq = Eq"}},{"before":null,"after":"4f338ca1fcdce7e03ea8dd5f066922b3e4aeb830","ref":"refs/heads/some_confusion","pushedAt":"2024-01-21T17:16:25.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"awalterschulze","name":"Walter Schulze","path":"/awalterschulze","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1829933?s=80&v=4"},"commit":{"message":"TEq = Eq\n\nIt is now possible to go between TEq and Eq\nNat is now TDecidable","shortMessageHtmlLink":"TEq = Eq"}},{"before":"185b9502300d84d16f0a138f50f80f06b6bb7f53","after":null,"ref":"refs/heads/session-2023-12-11","pushedAt":"2024-01-07T12:12:35.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"awalterschulze","name":"Walter Schulze","path":"/awalterschulze","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1829933?s=80&v=4"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"djE6ks8AAAAEFs0anwA","startCursor":null,"endCursor":null}},"title":"Activity · katydid/proofs"}