{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":720029965,"defaultBranch":"main","name":"cbpv-in-agda","ownerLogin":"plclub","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2023-11-17T12:32:42.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/4117335?v=4","public":true,"private":false,"isOrgOwned":true},"refInfo":{"name":"","listCacheKey":"v0:1700241302.0","currentOid":""},"activityList":{"items":[{"before":"f9ee801adf7acb5027b042138b3168ee660d9750","after":"c86fa56fca0556cff44f85c1c93a88b4b1339226","ref":"refs/heads/web","pushedAt":"2023-11-24T17:42:58.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"emmanueljs1","name":"Emmanuel Suárez Acevedo","path":"/emmanueljs1","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/19786004?s=80&v=4"},"commit":{"message":"update static stie","shortMessageHtmlLink":"update static stie"}},{"before":"6c7b168698207c7f1caad3dc993e694d9f2f989c","after":"8203b31d86bb0db94cf3c24c4b2d230cbbd140eb","ref":"refs/heads/main","pushedAt":"2023-11-24T17:41:07.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"emmanueljs1","name":"Emmanuel Suárez Acevedo","path":"/emmanueljs1","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/19786004?s=80&v=4"},"commit":{"message":"improve comments in everything.agda","shortMessageHtmlLink":"improve comments in everything.agda"}},{"before":null,"after":"f9ee801adf7acb5027b042138b3168ee660d9750","ref":"refs/heads/web","pushedAt":"2023-11-17T17:15:02.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"emmanueljs1","name":"Emmanuel Suárez Acevedo","path":"/emmanueljs1","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/19786004?s=80&v=4"},"commit":{"message":"static web files","shortMessageHtmlLink":"static web files"}},{"before":"c7fce02c702acd1dc7fcef9ee5c978a2b7b24bbb","after":"6c7b168698207c7f1caad3dc993e694d9f2f989c","ref":"refs/heads/main","pushedAt":"2023-11-17T17:07:15.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"emmanueljs1","name":"Emmanuel Suárez Acevedo","path":"/emmanueljs1","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/19786004?s=80&v=4"},"commit":{"message":"update everything.agda","shortMessageHtmlLink":"update everything.agda"}},{"before":"c0199f838e38be6b9672bd238eb504da10c69c13","after":"c7fce02c702acd1dc7fcef9ee5c978a2b7b24bbb","ref":"refs/heads/main","pushedAt":"2023-11-17T14:27:07.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"emmanueljs1","name":"Emmanuel Suárez Acevedo","path":"/emmanueljs1","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/19786004?s=80&v=4"},"commit":{"message":"add back agda version","shortMessageHtmlLink":"add back agda version"}},{"before":"304f4f459a4483c3332cc076f648836063fb71cc","after":"c0199f838e38be6b9672bd238eb504da10c69c13","ref":"refs/heads/main","pushedAt":"2023-11-17T14:25:36.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"emmanueljs1","name":"Emmanuel Suárez Acevedo","path":"/emmanueljs1","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/19786004?s=80&v=4"},"commit":{"message":"Remove assumption that pure <= phi for all phi","shortMessageHtmlLink":"Remove assumption that pure &lt;= phi for all phi"}},{"before":null,"after":"22763b4d1b8559c03e94f38ba70db8b6b28e2720","ref":"refs/heads/es/sub","pushedAt":"2023-11-17T14:24:40.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"emmanueljs1","name":"Emmanuel Suárez Acevedo","path":"/emmanueljs1","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/19786004?s=80&v=4"},"commit":{"message":"sub","shortMessageHtmlLink":"sub"}},{"before":null,"after":"65e77caa004b78dde7ed6e4656cc62c618cfe9dc","ref":"refs/heads/es/exp-2","pushedAt":"2023-11-17T14:24:40.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"emmanueljs1","name":"Emmanuel Suárez Acevedo","path":"/emmanueljs1","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/19786004?s=80&v=4"},"commit":{"message":"experiment adequacy w bigstep","shortMessageHtmlLink":"experiment adequacy w bigstep"}},{"before":null,"after":"66ef156a785f18327103d25d2bac667d194aacb6","ref":"refs/heads/coq","pushedAt":"2023-11-17T14:24:40.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"emmanueljs1","name":"Emmanuel Suárez Acevedo","path":"/emmanueljs1","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/19786004?s=80&v=4"},"commit":{"message":"move coq formalization to top level","shortMessageHtmlLink":"move coq formalization to top level"}},{"before":null,"after":"76c7a82f94ce83d7dfac6daf9eacb8c1ddd7a090","ref":"refs/heads/es/cbv","pushedAt":"2023-11-17T14:24:40.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"emmanueljs1","name":"Emmanuel Suárez Acevedo","path":"/emmanueljs1","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/19786004?s=80&v=4"},"commit":{"message":"CBV -> CBPV translation type preservation proof","shortMessageHtmlLink":"CBV -&gt; CBPV translation type preservation proof"}},{"before":null,"after":"7c53691cbf8c3da115b12e6a01c9149240e699d7","ref":"refs/heads/es/exp","pushedAt":"2023-11-17T14:24:40.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"emmanueljs1","name":"Emmanuel Suárez Acevedo","path":"/emmanueljs1","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/19786004?s=80&v=4"},"commit":{"message":"experiment with proving adequacy in other direction","shortMessageHtmlLink":"experiment with proving adequacy in other direction"}},{"before":null,"after":"a22dce9c2ba5f17f6a40e6a335bde12723e70644","ref":"refs/heads/es/sempres","pushedAt":"2023-11-17T14:24:40.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"emmanueljs1","name":"Emmanuel Suárez Acevedo","path":"/emmanueljs1","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/19786004?s=80&v=4"},"commit":{"message":"try proving CBN semantics preservation","shortMessageHtmlLink":"try proving CBN semantics preservation"}},{"before":null,"after":"c0199f838e38be6b9672bd238eb504da10c69c13","ref":"refs/heads/master","pushedAt":"2023-11-17T14:24:40.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"emmanueljs1","name":"Emmanuel Suárez Acevedo","path":"/emmanueljs1","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/19786004?s=80&v=4"},"commit":{"message":"Remove assumption that pure <= phi for all phi","shortMessageHtmlLink":"Remove assumption that pure &lt;= phi for all phi"}},{"before":null,"after":"f8bb51c5b0f73c626472ea911dd55baf754cd22d","ref":"refs/heads/CBV-CBPV","pushedAt":"2023-11-17T14:24:40.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"emmanueljs1","name":"Emmanuel Suárez Acevedo","path":"/emmanueljs1","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/19786004?s=80&v=4"},"commit":{"message":"Remove additional","shortMessageHtmlLink":"Remove additional"}},{"before":null,"after":"fa840d8be1400f986b86daca1dcbbb139e82269a","ref":"refs/heads/oopsla24","pushedAt":"2023-11-17T14:24:40.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"emmanueljs1","name":"Emmanuel Suárez Acevedo","path":"/emmanueljs1","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/19786004?s=80&v=4"},"commit":{"message":"oopsla24 artifact","shortMessageHtmlLink":"oopsla24 artifact"}},{"before":"1ef8ec101564f48bd17805b66932ccf87f5f4d68","after":"304f4f459a4483c3332cc076f648836063fb71cc","ref":"refs/heads/main","pushedAt":"2023-11-17T12:42:37.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"sweirich","name":"Stephanie Weirich","path":"/sweirich","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2103670?s=80&v=4"},"commit":{"message":"agda version","shortMessageHtmlLink":"agda version"}},{"before":null,"after":"1ef8ec101564f48bd17805b66932ccf87f5f4d68","ref":"refs/heads/main","pushedAt":"2023-11-17T12:36:33.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"sweirich","name":"Stephanie Weirich","path":"/sweirich","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/2103670?s=80&v=4"},"commit":{"message":"initial commit","shortMessageHtmlLink":"initial commit"}}],"hasNextPage":false,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"djE6ks8AAAADtxPfRQA","startCursor":null,"endCursor":null}},"title":"Activity · plclub/cbpv-in-agda"}