{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":277587435,"defaultBranch":"master","name":"grove-agda","ownerLogin":"fplab","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2020-07-06T16:01:58.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/54806763?v=4","public":true,"private":false,"isOrgOwned":true},"refInfo":{"name":"","listCacheKey":"v0:1720554970.0","currentOid":""},"activityList":{"items":[{"before":"b280070850e7d74c7dea84fe2de0b4b78fc3a01d","after":"dd21e9b19ffdc5a88597871c32ef50c5c2725d1f","ref":"refs/heads/master","pushedAt":"2024-07-12T09:36:14.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"thomasporter522","name":"Thomas Porter","path":"/thomasporter522","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/22896135?s=80&v=4"},"commit":{"message":"updated readme","shortMessageHtmlLink":"updated readme"}},{"before":"91daeeccd40e7a2c583053a0646732d4d67ce76b","after":"b280070850e7d74c7dea84fe2de0b4b78fc3a01d","ref":"refs/heads/master","pushedAt":"2024-07-12T07:31:35.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"thomasporter522","name":"Thomas Porter","path":"/thomasporter522","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/22896135?s=80&v=4"},"commit":{"message":"updated readme","shortMessageHtmlLink":"updated readme"}},{"before":"8e0cbf917a0ab9af291e5c74413e3038854d6958","after":"91daeeccd40e7a2c583053a0646732d4d67ce76b","ref":"refs/heads/master","pushedAt":"2024-07-12T06:09:13.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"thomasporter522","name":"Thomas Porter","path":"/thomasporter522","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/22896135?s=80&v=4"},"commit":{"message":"termination caveats","shortMessageHtmlLink":"termination caveats"}},{"before":"ccbb9add5695ba7c8f73bc5de27dfd2e037e9dd4","after":"8e0cbf917a0ab9af291e5c74413e3038854d6958","ref":"refs/heads/master","pushedAt":"2024-07-12T05:59:09.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"thomasporter522","name":"Thomas Porter","path":"/thomasporter522","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/22896135?s=80&v=4"},"commit":{"message":"cleanup and termination argument","shortMessageHtmlLink":"cleanup and termination argument"}},{"before":"39569c5289628dc91e415abc3e98175d9a73f7fc","after":"ccbb9add5695ba7c8f73bc5de27dfd2e037e9dd4","ref":"refs/heads/master","pushedAt":"2024-07-12T01:38:47.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"svishnus","name":"Sundara Vishnu","path":"/svishnus","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/55348287?s=80&v=4"},"commit":{"message":"fix: typos and clarity","shortMessageHtmlLink":"fix: typos and clarity"}},{"before":"9918adcf100fdbf8a5503062f99d41e1dcbf26c8","after":"39569c5289628dc91e415abc3e98175d9a73f7fc","ref":"refs/heads/master","pushedAt":"2024-07-12T01:28:47.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"svishnus","name":"Sundara Vishnu","path":"/svishnus","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/55348287?s=80&v=4"},"commit":{"message":"feat: top level README, marking info","shortMessageHtmlLink":"feat: top level README, marking info"}},{"before":"a0b6ad5ebbbaba0add2470802cd3dc2d8e287479","after":"9918adcf100fdbf8a5503062f99d41e1dcbf26c8","ref":"refs/heads/master","pushedAt":"2024-07-11T23:13:57.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"mirryi","name":"Eric Zhao","path":"/mirryi","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/38477923?s=80&v=4"},"commit":{"message":"rename TermList to ChildTerm","shortMessageHtmlLink":"rename TermList to ChildTerm"}},{"before":"03cfd66a9b862bccd077c99af06fd525bc207080","after":"a0b6ad5ebbbaba0add2470802cd3dc2d8e287479","ref":"refs/heads/master","pushedAt":"2024-07-11T23:07:03.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"mirryi","name":"Eric Zhao","path":"/mirryi","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/38477923?s=80&v=4"},"commit":{"message":"rename Source to Location","shortMessageHtmlLink":"rename Source to Location"}},{"before":"75d12e2b6a43317dd7d133a1d37f2b53ad16c9ba","after":"03cfd66a9b862bccd077c99af06fd525bc207080","ref":"refs/heads/master","pushedAt":"2024-07-11T22:55:56.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"mirryi","name":"Eric Zhao","path":"/mirryi","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/38477923?s=80&v=4"},"commit":{"message":"fix the proofs!","shortMessageHtmlLink":"fix the proofs!"}},{"before":"5e7ec674ffa290e7dd46ebef076e87b4e02fdd89","after":"75d12e2b6a43317dd7d133a1d37f2b53ad16c9ba","ref":"refs/heads/master","pushedAt":"2024-07-11T21:22:57.000Z","pushType":"push","commitsCount":4,"pusher":{"login":"mirryi","name":"Eric Zhao","path":"/mirryi","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/38477923?s=80&v=4"},"commit":{"message":"analytic rules for location conflicts","shortMessageHtmlLink":"analytic rules for location conflicts"}},{"before":"cce5f0504d64c747ca919106e45a1fa70fc9360a","after":"5e7ec674ffa290e7dd46ebef076e87b4e02fdd89","ref":"refs/heads/master","pushedAt":"2024-07-11T20:38:07.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"mirryi","name":"Eric Zhao","path":"/mirryi","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/38477923?s=80&v=4"},"commit":{"message":"more renamings","shortMessageHtmlLink":"more renamings"}},{"before":"1dd23a8815948aa3fdf0e438042a1615f89d73ba","after":"cce5f0504d64c747ca919106e45a1fa70fc9360a","ref":"refs/heads/master","pushedAt":"2024-07-11T18:08:43.000Z","pushType":"push","commitsCount":118,"pusher":{"login":"thomasporter522","name":"Thomas Porter","path":"/thomasporter522","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/22896135?s=80&v=4"},"commit":{"message":"removed extra function from decomp","shortMessageHtmlLink":"removed extra function from decomp"}},{"before":"83b0978b2f17f64aa660287feaddb8eb4aa95c8f","after":"cce5f0504d64c747ca919106e45a1fa70fc9360a","ref":"refs/heads/marking-split","pushedAt":"2024-07-11T16:29:37.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"thomasporter522","name":"Thomas Porter","path":"/thomasporter522","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/22896135?s=80&v=4"},"commit":{"message":"removed extra function from decomp","shortMessageHtmlLink":"removed extra function from decomp"}},{"before":"592c33760486aabf39c800b44f67a5c527b7eb9c","after":"83b0978b2f17f64aa660287feaddb8eb4aa95c8f","ref":"refs/heads/marking-split","pushedAt":"2024-07-10T21:36:12.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"mirryi","name":"Eric Zhao","path":"/mirryi","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/38477923?s=80&v=4"},"commit":{"message":"wip correspondence","shortMessageHtmlLink":"wip correspondence"}},{"before":"754646cecf20c15f39c4faab2ef9301155503fff","after":"592c33760486aabf39c800b44f67a5c527b7eb9c","ref":"refs/heads/marking-split","pushedAt":"2024-07-10T20:07:24.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"thomasporter522","name":"Thomas Porter","path":"/thomasporter522","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/22896135?s=80&v=4"},"commit":{"message":"Merge branch 'marking-split' of https://github.com/fplab/grove-agda into marking-split","shortMessageHtmlLink":"Merge branch 'marking-split' of <a href=\"https://github.com/fplab/grove-agda\">https://github.com/fplab/grove-agda</a> i…"}},{"before":"e6e71bca820184dedaf430ed6e52631cd63596c1","after":"754646cecf20c15f39c4faab2ef9301155503fff","ref":"refs/heads/marking-split","pushedAt":"2024-07-10T20:00:25.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"mirryi","name":"Eric Zhao","path":"/mirryi","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/38477923?s=80&v=4"},"commit":{"message":"add ctors for types","shortMessageHtmlLink":"add ctors for types"}},{"before":"8f505454c0c65b54c1ec7c3657aa8b398d87762f","after":"e6e71bca820184dedaf430ed6e52631cd63596c1","ref":"refs/heads/marking-split","pushedAt":"2024-07-10T19:57:55.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"mirryi","name":"Eric Zhao","path":"/mirryi","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/38477923?s=80&v=4"},"commit":{"message":"fix lambda type annotation to be GSubTyp","shortMessageHtmlLink":"fix lambda type annotation to be GSubTyp"}},{"before":"7dbc97543e59cf62a776159f80d2dec10a118aae","after":"8f505454c0c65b54c1ec7c3657aa8b398d87762f","ref":"refs/heads/marking-split","pushedAt":"2024-07-10T17:05:02.000Z","pushType":"push","commitsCount":3,"pusher":{"login":"mirryi","name":"Eric Zhao","path":"/mirryi","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/38477923?s=80&v=4"},"commit":{"message":"more refactor, fix term structure","shortMessageHtmlLink":"more refactor, fix term structure"}},{"before":"5c90ed73257583c58239eb2542c4e9033c0c4e87","after":"7dbc97543e59cf62a776159f80d2dec10a118aae","ref":"refs/heads/marking-split","pushedAt":"2024-07-10T14:31:04.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"mirryi","name":"Eric Zhao","path":"/mirryi","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/38477923?s=80&v=4"},"commit":{"message":"move core under Grove namespace","shortMessageHtmlLink":"move core under Grove namespace"}},{"before":"0e8696c768a7629fece0819c685193f7bcfef868","after":"5c90ed73257583c58239eb2542c4e9033c0c4e87","ref":"refs/heads/marking-split","pushedAt":"2024-07-10T14:03:59.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"mirryi","name":"Eric Zhao","path":"/mirryi","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/38477923?s=80&v=4"},"commit":{"message":"start to add grove instantiation","shortMessageHtmlLink":"start to add grove instantiation"}},{"before":"75d07971cdae146fd6a4a4f42d8c55a78b4a80db","after":"0e8696c768a7629fece0819c685193f7bcfef868","ref":"refs/heads/marking-split","pushedAt":"2024-07-10T13:15:14.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"mirryi","name":"Eric Zhao","path":"/mirryi","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/38477923?s=80&v=4"},"commit":{"message":"redo module naming","shortMessageHtmlLink":"redo module naming"}},{"before":"f4f3ee890dafdae4bc5225c6e4560829c868c251","after":"b0eb4f907482bca9a6c9faa758112672a3007221","ref":"refs/heads/simpler","pushedAt":"2024-07-10T04:50:46.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"thomasporter522","name":"Thomas Porter","path":"/thomasporter522","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/22896135?s=80&v=4"},"commit":{"message":"added example language syntactic equivalence proof","shortMessageHtmlLink":"added example language syntactic equivalence proof"}},{"before":"c000b8ba9537703700623235bf414c84d2007267","after":"f4f3ee890dafdae4bc5225c6e4560829c868c251","ref":"refs/heads/simpler","pushedAt":"2024-07-10T04:13:26.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"thomasporter522","name":"Thomas Porter","path":"/thomasporter522","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/22896135?s=80&v=4"},"commit":{"message":"some kind of module parametricity","shortMessageHtmlLink":"some kind of module parametricity"}},{"before":"dc692b438b40bd48d92e2b25e10c6df70900c31e","after":"c000b8ba9537703700623235bf414c84d2007267","ref":"refs/heads/simpler","pushedAt":"2024-07-10T03:49:19.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"thomasporter522","name":"Thomas Porter","path":"/thomasporter522","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/22896135?s=80&v=4"},"commit":{"message":"updated term representation","shortMessageHtmlLink":"updated term representation"}},{"before":"c3d782e4f7b815a045b43164be8db85d254768fd","after":"dc692b438b40bd48d92e2b25e10c6df70900c31e","ref":"refs/heads/simpler","pushedAt":"2024-07-09T23:32:38.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"thomasporter522","name":"Thomas Porter","path":"/thomasporter522","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/22896135?s=80&v=4"},"commit":{"message":"fixed unique id issue","shortMessageHtmlLink":"fixed unique id issue"}},{"before":"569a99ed058627fc231406f50e9abc60d7a867d0","after":"75d07971cdae146fd6a4a4f42d8c55a78b4a80db","ref":"refs/heads/marking-split","pushedAt":"2024-07-09T23:14:30.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"mirryi","name":"Eric Zhao","path":"/mirryi","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/38477923?s=80&v=4"},"commit":{"message":"redo module naming","shortMessageHtmlLink":"redo module naming"}},{"before":"8a35ccddbd0a222acd24dd120d08eb8a479b7298","after":"c3d782e4f7b815a045b43164be8db85d254768fd","ref":"refs/heads/simpler","pushedAt":"2024-07-09T22:30:52.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"thomasporter522","name":"Thomas Porter","path":"/thomasporter522","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/22896135?s=80&v=4"},"commit":{"message":"standard library only","shortMessageHtmlLink":"standard library only"}},{"before":"8fbe5479bccceb1ea701279b07f9674a482064b0","after":"8a35ccddbd0a222acd24dd120d08eb8a479b7298","ref":"refs/heads/simpler","pushedAt":"2024-07-09T22:10:57.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"thomasporter522","name":"Thomas Porter","path":"/thomasporter522","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/22896135?s=80&v=4"},"commit":{"message":"distinct vertex and edge ids","shortMessageHtmlLink":"distinct vertex and edge ids"}},{"before":"cdce8dc3a3367c952086904a5ba382978dc4f5b0","after":"8fbe5479bccceb1ea701279b07f9674a482064b0","ref":"refs/heads/simpler","pushedAt":"2024-07-09T21:40:56.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"thomasporter522","name":"Thomas Porter","path":"/thomasporter522","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/22896135?s=80&v=4"},"commit":{"message":"begin parameters","shortMessageHtmlLink":"begin parameters"}},{"before":"dc460617ec994c9b9643acea9f35f3f3b2c40962","after":"cdce8dc3a3367c952086904a5ba382978dc4f5b0","ref":"refs/heads/simpler","pushedAt":"2024-07-09T20:03:07.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"thomasporter522","name":"Thomas Porter","path":"/thomasporter522","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/22896135?s=80&v=4"},"commit":{"message":"completed decomp recomp up to fuel","shortMessageHtmlLink":"completed decomp recomp up to fuel"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"djE6ks8AAAAEfbCpdgA","startCursor":null,"endCursor":null}},"title":"Activity · fplab/grove-agda"}