{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":757222550,"defaultBranch":"develop","name":"HOL","ownerLogin":"Gordon-Sau","currentUserCanPush":false,"isFork":true,"isEmpty":false,"createdAt":"2024-02-14T03:27:05.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/66369887?v=4","public":true,"private":false,"isOrgOwned":false},"refInfo":{"name":"","listCacheKey":"v0:1710232969.0","currentOid":""},"activityList":{"items":[{"before":"772a64a23fab01445886a113b810bd3c02930e63","after":"9e8cb30bf8756b6c7bae0ca2ba897b7344026c18","ref":"refs/heads/develop","pushedAt":"2024-03-25T01:09:18.000Z","pushType":"push","commitsCount":57,"pusher":{"login":"Gordon-Sau","name":null,"path":"/Gordon-Sau","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/66369887?s=80&v=4"},"commit":{"message":"Start of some work on \"algebras as types\"\n\nStarting with the base of the algebra pyramid keeps things simpler,\nand will hopefully allow the technology to be worked out and polished.","shortMessageHtmlLink":"Start of some work on \"algebras as types\""}},{"before":"14e9458b0e62c6a613243213eec43ce979caa4ea","after":"772a64a23fab01445886a113b810bd3c02930e63","ref":"refs/heads/develop","pushedAt":"2024-03-25T01:08:30.000Z","pushType":"push","commitsCount":34,"pusher":{"login":"Gordon-Sau","name":null,"path":"/Gordon-Sau","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/66369887?s=80&v=4"},"commit":{"message":"Tweak tailrecLib to allow function terms that are composite\n\nOld behaviour required the fn_t to be a single atomic term  (variable\nor constant), which allows the code looking for fn_t to call\nstrip_comb. But if fn_t is a composite (like ``f x`` for an unvarying\nargument ``x``, then that approach breaks.","shortMessageHtmlLink":"Tweak tailrecLib to allow function terms that are composite"}},{"before":"abd41db6cf9238bb8e5dcc021ed838d37c69facc","after":null,"ref":"refs/heads/WF_PULL","pushedAt":"2024-03-12T08:42:49.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"Gordon-Sau","name":null,"path":"/Gordon-Sau","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/66369887?s=80&v=4"}},{"before":"7d471066f1dfc7d6707bf6b36e7c1f869bf0a19f","after":"abd41db6cf9238bb8e5dcc021ed838d37c69facc","ref":"refs/heads/WF_PULL","pushedAt":"2024-03-06T07:25:01.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Gordon-Sau","name":null,"path":"/Gordon-Sau","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/66369887?s=80&v=4"},"commit":{"message":"avoid using bossLib","shortMessageHtmlLink":"avoid using bossLib"}},{"before":"22406ea667e3c073f45a5f4109adf8ca9533e1fc","after":"7d471066f1dfc7d6707bf6b36e7c1f869bf0a19f","ref":"refs/heads/WF_PULL","pushedAt":"2024-03-06T06:30:39.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"Gordon-Sau","name":null,"path":"/Gordon-Sau","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/66369887?s=80&v=4"},"commit":{"message":"add WF_PULL to relationTheory","shortMessageHtmlLink":"add WF_PULL to relationTheory"}},{"before":"c6f8f258011d65af729f8d1a0583440336c17b34","after":"22406ea667e3c073f45a5f4109adf8ca9533e1fc","ref":"refs/heads/WF_PULL","pushedAt":"2024-03-06T06:26:37.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"Gordon-Sau","name":null,"path":"/Gordon-Sau","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/66369887?s=80&v=4"},"commit":{"message":"add WF_PULL to relationTheory","shortMessageHtmlLink":"add WF_PULL to relationTheory"}},{"before":"48fabbd05a40fa3a5cd84ce24cac2cc7a8358ea0","after":null,"ref":"refs/heads/cycle_detection","pushedAt":"2024-03-06T06:10:26.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"Gordon-Sau","name":null,"path":"/Gordon-Sau","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/66369887?s=80&v=4"}},{"before":"772a64a23fab01445886a113b810bd3c02930e63","after":"c6f8f258011d65af729f8d1a0583440336c17b34","ref":"refs/heads/WF_PULL","pushedAt":"2024-03-06T06:10:11.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Gordon-Sau","name":null,"path":"/Gordon-Sau","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/66369887?s=80&v=4"},"commit":{"message":"add WF_PULL to relationTheory","shortMessageHtmlLink":"add WF_PULL to relationTheory"}},{"before":null,"after":"772a64a23fab01445886a113b810bd3c02930e63","ref":"refs/heads/WF_PULL","pushedAt":"2024-03-06T06:08:35.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"Gordon-Sau","name":null,"path":"/Gordon-Sau","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/66369887?s=80&v=4"},"commit":{"message":"Tweak tailrecLib to allow function terms that are composite\n\nOld behaviour required the fn_t to be a single atomic term  (variable\nor constant), which allows the code looking for fn_t to call\nstrip_comb. But if fn_t is a composite (like ``f x`` for an unvarying\nargument ``x``, then that approach breaks.","shortMessageHtmlLink":"Tweak tailrecLib to allow function terms that are composite"}},{"before":"4738fd9c9c23c161a2aedd0fc09096cf8d3e415a","after":"48fabbd05a40fa3a5cd84ce24cac2cc7a8358ea0","ref":"refs/heads/cycle_detection","pushedAt":"2024-02-16T04:54:39.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Gordon-Sau","name":null,"path":"/Gordon-Sau","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/66369887?s=80&v=4"},"commit":{"message":"remove whitespace","shortMessageHtmlLink":"remove whitespace"}},{"before":"1fc03f99a7708598f6eeacd97634a0383164d154","after":"4738fd9c9c23c161a2aedd0fc09096cf8d3e415a","ref":"refs/heads/cycle_detection","pushedAt":"2024-02-15T20:19:47.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Gordon-Sau","name":null,"path":"/Gordon-Sau","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/66369887?s=80&v=4"},"commit":{"message":"topological_sort: prove that every partition is a SCC (strongly connectedd component)","shortMessageHtmlLink":"topological_sort: prove that every partition is a SCC (strongly conne…"}},{"before":null,"after":"1fc03f99a7708598f6eeacd97634a0383164d154","ref":"refs/heads/cycle_detection","pushedAt":"2024-02-14T03:27:52.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"Gordon-Sau","name":null,"path":"/Gordon-Sau","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/66369887?s=80&v=4"},"commit":{"message":"add theorems for cycle detection to topological_sortTheory","shortMessageHtmlLink":"add theorems for cycle detection to topological_sortTheory"}}],"hasNextPage":false,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"djE6ks8AAAAEHiDakAA","startCursor":null,"endCursor":null}},"title":"Activity · Gordon-Sau/HOL"}