{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":470204772,"defaultBranch":"master","name":"QpfTypes","ownerLogin":"alexkeizer","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2022-03-15T14:48:15.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/18490187?v=4","public":true,"private":false,"isOrgOwned":false},"refInfo":{"name":"","listCacheKey":"v0:1723828341.0","currentOid":""},"activityList":{"items":[{"before":"5ace7ca1101a1a8ee25a90f030edf245ef30e577","after":"5413c5a3c951ff9d29ef2fd8b4a0d1ea03521e7f","ref":"refs/heads/master","pushedAt":"2024-08-22T14:26:58.000Z","pushType":"pr_merge","commitsCount":3,"pusher":{"login":"alexkeizer","name":"Alex Keizer","path":"/alexkeizer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/18490187?s=80&v=4"},"commit":{"message":"refactor: review comments","shortMessageHtmlLink":"refactor: review comments"}},{"before":"da2df6295974b636809cc9c3c88d101e4fbbedbf","after":"65a20469157c927a94acfe7468dd468d4ac8d98a","ref":"refs/heads/add-notion-of-a-deep-thunk","pushedAt":"2024-08-22T14:24:42.000Z","pushType":"push","commitsCount":18,"pusher":{"login":"alexkeizer","name":"Alex Keizer","path":"/alexkeizer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/18490187?s=80&v=4"},"commit":{"message":"Merge branch 'master' into add-notion-of-a-deep-thunk","shortMessageHtmlLink":"Merge branch 'master' into add-notion-of-a-deep-thunk"}},{"before":"1d6f6caaea0b120a3f6c1a4ca6bc713a24e81e35","after":"04ddc92520dc2eb8b99473c645b012cb7015787f","ref":"refs/heads/coinductive-predicates","pushedAt":"2024-08-20T12:08:12.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Equilibris","name":"William Sørensen","path":"/Equilibris","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/47296141?s=80&v=4"},"commit":{"message":"refactor: change generation to use inductives underneath to allow for simpler defns","shortMessageHtmlLink":"refactor: change generation to use inductives underneath to allow for…"}},{"before":"33a3b9e5cb7417f9ec90ecabf565b7097133e7a7","after":"1d6f6caaea0b120a3f6c1a4ca6bc713a24e81e35","ref":"refs/heads/coinductive-predicates","pushedAt":"2024-08-19T17:28:20.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Equilibris","name":"William Sørensen","path":"/Equilibris","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/47296141?s=80&v=4"},"commit":{"message":"fix: predicate generation","shortMessageHtmlLink":"fix: predicate generation"}},{"before":"b225e07c7c7d40c1ca662b5140613f47c4fb7f89","after":"5ace7ca1101a1a8ee25a90f030edf245ef30e577","ref":"refs/heads/master","pushedAt":"2024-08-19T12:51:19.000Z","pushType":"pr_merge","commitsCount":7,"pusher":{"login":"Equilibris","name":"William Sørensen","path":"/Equilibris","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/47296141?s=80&v=4"},"commit":{"message":"Merge pull request #40 from alexkeizer/generalize-constructor-generation-further\n\nfeat: generalize constructor generation further","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2469958181\" data-permission-text=\"Title is private\" data-url=\"https://github.com/alexkeizer/QpfTypes/issues/40\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/alexkeizer/QpfTypes/pull/40/hovercard\" href=\"https://github.com/alexkeizer/QpfTypes/pull/40\">#40</a> from alexkeizer/generalize-constructor-generat…"}},{"before":"887ce8074ad38ef8b28426e93c91870507a52c6d","after":"f902d4e53d54d36f742c3fdf971131f03d269e94","ref":"refs/heads/generalize-constructor-generation-further","pushedAt":"2024-08-19T12:49:19.000Z","pushType":"push","commitsCount":10,"pusher":{"login":"Equilibris","name":"William Sørensen","path":"/Equilibris","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/47296141?s=80&v=4"},"commit":{"message":"Merge branch 'master' into generalize-constructor-generation-further","shortMessageHtmlLink":"Merge branch 'master' into generalize-constructor-generation-further"}},{"before":"c742a6bb35258a1bb8ff831ea344b7d4976a5292","after":"da2df6295974b636809cc9c3c88d101e4fbbedbf","ref":"refs/heads/add-notion-of-a-deep-thunk","pushedAt":"2024-08-19T12:47:34.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"Equilibris","name":"William Sørensen","path":"/Equilibris","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/47296141?s=80&v=4"},"commit":{"message":"refactor: review comments","shortMessageHtmlLink":"refactor: review comments"}},{"before":"78cfd1593eb6a274d346f351b6f31e8aa5f4f01e","after":"c742a6bb35258a1bb8ff831ea344b7d4976a5292","ref":"refs/heads/add-notion-of-a-deep-thunk","pushedAt":"2024-08-19T12:45:44.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Equilibris","name":"William Sørensen","path":"/Equilibris","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/47296141?s=80&v=4"},"commit":{"message":"refactor: review comments","shortMessageHtmlLink":"refactor: review comments"}},{"before":"c4b021dfd3e462a77cb37ba349528cf4b0fe8ce1","after":"78cfd1593eb6a274d346f351b6f31e8aa5f4f01e","ref":"refs/heads/add-notion-of-a-deep-thunk","pushedAt":"2024-08-19T12:39:02.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Equilibris","name":"William Sørensen","path":"/Equilibris","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/47296141?s=80&v=4"},"commit":{"message":"refactor: review comments","shortMessageHtmlLink":"refactor: review comments"}},{"before":"89b86d26c7301f0adb1bcc621c870f9d238ca308","after":"887ce8074ad38ef8b28426e93c91870507a52c6d","ref":"refs/heads/generalize-constructor-generation-further","pushedAt":"2024-08-19T12:07:57.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"Equilibris","name":"William Sørensen","path":"/Equilibris","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/47296141?s=80&v=4"},"commit":{"message":"Merge remote-tracking branch 'refs/remotes/origin/generalize-constructor-generation-further' into generalize-constructor-generation-further","shortMessageHtmlLink":"Merge remote-tracking branch 'refs/remotes/origin/generalize-construc…"}},{"before":"b490634845de9ce1c7710e00193691a489c07180","after":"b225e07c7c7d40c1ca662b5140613f47c4fb7f89","ref":"refs/heads/master","pushedAt":"2024-08-17T18:34:33.000Z","pushType":"pr_merge","commitsCount":4,"pusher":{"login":"Equilibris","name":"William Sørensen","path":"/Equilibris","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/47296141?s=80&v=4"},"commit":{"message":"Merge pull request #39 from alexkeizer/cleanup-ind\n\nrefactor: prefer concat (++) over hand crafting names","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2469948060\" data-permission-text=\"Title is private\" data-url=\"https://github.com/alexkeizer/QpfTypes/issues/39\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/alexkeizer/QpfTypes/pull/39/hovercard\" href=\"https://github.com/alexkeizer/QpfTypes/pull/39\">#39</a> from alexkeizer/cleanup-ind"}},{"before":"67f47bdb5bc49b6fa9c1a07e23e020f7536aa4ea","after":"565fbe4c88f25407863961fb0bd287c17a52decc","ref":"refs/heads/cleanup-ind","pushedAt":"2024-08-17T18:32:28.000Z","pushType":"push","commitsCount":5,"pusher":{"login":"Equilibris","name":"William Sørensen","path":"/Equilibris","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/47296141?s=80&v=4"},"commit":{"message":"Merge branch 'master' into cleanup-ind","shortMessageHtmlLink":"Merge branch 'master' into cleanup-ind"}},{"before":"2960ed4ea48ec673d269cb0c855c56968e668cbc","after":"b490634845de9ce1c7710e00193691a489c07180","ref":"refs/heads/master","pushedAt":"2024-08-17T11:35:26.000Z","pushType":"pr_merge","commitsCount":4,"pusher":{"login":"Equilibris","name":"William Sørensen","path":"/Equilibris","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/47296141?s=80&v=4"},"commit":{"message":"Merge pull request #37 from alexkeizer/expose-curried-base\n\nfeat: add the ability to access the uncurried base","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2469905397\" data-permission-text=\"Title is private\" data-url=\"https://github.com/alexkeizer/QpfTypes/issues/37\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/alexkeizer/QpfTypes/pull/37/hovercard\" href=\"https://github.com/alexkeizer/QpfTypes/pull/37\">#37</a> from alexkeizer/expose-curried-base"}},{"before":"628c7e68a7bc3ccef9e63ac0e72287bc25db8101","after":"67f47bdb5bc49b6fa9c1a07e23e020f7536aa4ea","ref":"refs/heads/cleanup-ind","pushedAt":"2024-08-17T11:34:29.000Z","pushType":"push","commitsCount":3,"pusher":{"login":"Equilibris","name":"William Sørensen","path":"/Equilibris","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/47296141?s=80&v=4"},"commit":{"message":"Merge branch 'master' into cleanup-ind","shortMessageHtmlLink":"Merge branch 'master' into cleanup-ind"}},{"before":"633e2c06eef9790fbfdeb8f04949472010d3394a","after":"12f1d9bf34939b3e7d19df540f4794f61f296e9f","ref":"refs/heads/expose-curried-base","pushedAt":"2024-08-17T11:33:19.000Z","pushType":"push","commitsCount":3,"pusher":{"login":"Equilibris","name":"William Sørensen","path":"/Equilibris","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/47296141?s=80&v=4"},"commit":{"message":"Merge branch 'master' into expose-curried-base","shortMessageHtmlLink":"Merge branch 'master' into expose-curried-base"}},{"before":"393d5e27f97608d4d63eadfc953e4d46b40e908c","after":"2960ed4ea48ec673d269cb0c855c56968e668cbc","ref":"refs/heads/master","pushedAt":"2024-08-17T11:27:53.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"Equilibris","name":"William Sørensen","path":"/Equilibris","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/47296141?s=80&v=4"},"commit":{"message":"Merge pull request #38 from alexkeizer/extract-rec-form-handling\n\nrefactor: extract handling of RecForms","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2469928801\" data-permission-text=\"Title is private\" data-url=\"https://github.com/alexkeizer/QpfTypes/issues/38\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/alexkeizer/QpfTypes/pull/38/hovercard\" href=\"https://github.com/alexkeizer/QpfTypes/pull/38\">#38</a> from alexkeizer/extract-rec-form-handling"}},{"before":"3a2949ea63f21e2cca3c66ac33f68075e431b2fb","after":"633e2c06eef9790fbfdeb8f04949472010d3394a","ref":"refs/heads/expose-curried-base","pushedAt":"2024-08-17T11:27:32.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Equilibris","name":"William Sørensen","path":"/Equilibris","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/47296141?s=80&v=4"},"commit":{"message":"Update Qpf/Macro/Data.lean\n\nCo-authored-by: Alex Keizer <alex@keizer.dev>","shortMessageHtmlLink":"Update Qpf/Macro/Data.lean"}},{"before":"a554c918448b50b5212a2312d2f2aec719dcede4","after":"33a3b9e5cb7417f9ec90ecabf565b7097133e7a7","ref":"refs/heads/coinductive-predicates","pushedAt":"2024-08-17T04:33:56.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"alexkeizer","name":"Alex Keizer","path":"/alexkeizer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/18490187?s=80&v=4"},"commit":{"message":"de-Mathlibify examples","shortMessageHtmlLink":"de-Mathlibify examples"}},{"before":"b5f490dad49138ea91e874481a8bfe3c5e3c187a","after":"a554c918448b50b5212a2312d2f2aec719dcede4","ref":"refs/heads/coinductive-predicates","pushedAt":"2024-08-17T03:46:06.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"alexkeizer","name":"Alex Keizer","path":"/alexkeizer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/18490187?s=80&v=4"},"commit":{"message":"unary coinductive predicate example","shortMessageHtmlLink":"unary coinductive predicate example"}},{"before":"a5b22d5257230e8a42c7a43ca047ee1405ad85f2","after":"b5f490dad49138ea91e874481a8bfe3c5e3c187a","ref":"refs/heads/coinductive-predicates","pushedAt":"2024-08-17T03:42:40.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"alexkeizer","name":"Alex Keizer","path":"/alexkeizer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/18490187?s=80&v=4"},"commit":{"message":"hacked together `coinduction` tactic","shortMessageHtmlLink":"hacked together <code>coinduction</code> tactic"}},{"before":"525a292104d0388744f2945d62ddd12b9c0a691d","after":"a5b22d5257230e8a42c7a43ca047ee1405ad85f2","ref":"refs/heads/coinductive-predicates","pushedAt":"2024-08-17T03:27:28.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"alexkeizer","name":"Alex Keizer","path":"/alexkeizer","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/18490187?s=80&v=4"},"commit":{"message":"Failing test case for WeakBisim","shortMessageHtmlLink":"Failing test case for WeakBisim"}},{"before":"015df095a41d497754f358286b1797ad03f84abb","after":"525a292104d0388744f2945d62ddd12b9c0a691d","ref":"refs/heads/coinductive-predicates","pushedAt":"2024-08-16T18:23:36.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Equilibris","name":"William Sørensen","path":"/Equilibris","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/47296141?s=80&v=4"},"commit":{"message":"chore: add guard_msgs to tests","shortMessageHtmlLink":"chore: add guard_msgs to tests"}},{"before":null,"after":"015df095a41d497754f358286b1797ad03f84abb","ref":"refs/heads/coinductive-predicates","pushedAt":"2024-08-16T17:12:21.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"Equilibris","name":"William Sørensen","path":"/Equilibris","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/47296141?s=80&v=4"},"commit":{"message":"faet: basic coind predicates","shortMessageHtmlLink":"faet: basic coind predicates"}},{"before":"c6ee24d5a26a9ffdb93670928e7cd0b2a2fca52a","after":"89b86d26c7301f0adb1bcc621c870f9d238ca308","ref":"refs/heads/generalize-constructor-generation-further","pushedAt":"2024-08-16T12:19:41.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Equilibris","name":"William Sørensen","path":"/Equilibris","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/47296141?s=80&v=4"},"commit":{"message":"Update Qpf/Macro/Data/Constructors.lean\n\nCo-authored-by: Atticus Kuhn <52258164+AtticusKuhn@users.noreply.github.com>","shortMessageHtmlLink":"Update Qpf/Macro/Data/Constructors.lean"}},{"before":null,"after":"c4b021dfd3e462a77cb37ba349528cf4b0fe8ce1","ref":"refs/heads/add-notion-of-a-deep-thunk","pushedAt":"2024-08-16T10:32:24.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"Equilibris","name":"William Sørensen","path":"/Equilibris","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/47296141?s=80&v=4"},"commit":{"message":"feat: add DeepThunk","shortMessageHtmlLink":"feat: add DeepThunk"}},{"before":"ab6aa44f27dcc67cf6e3bbd23aa66bd1b88a9c9d","after":"c6ee24d5a26a9ffdb93670928e7cd0b2a2fca52a","ref":"refs/heads/generalize-constructor-generation-further","pushedAt":"2024-08-16T10:09:09.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"Equilibris","name":"William Sørensen","path":"/Equilibris","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/47296141?s=80&v=4"},"commit":{"message":"Merge branch 'extract-rec-form-handling' into generalize-constructor-generation-further","shortMessageHtmlLink":"Merge branch 'extract-rec-form-handling' into generalize-constructor-…"}},{"before":null,"after":"628c7e68a7bc3ccef9e63ac0e72287bc25db8101","ref":"refs/heads/cleanup-ind","pushedAt":"2024-08-16T10:05:12.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"Equilibris","name":"William Sørensen","path":"/Equilibris","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/47296141?s=80&v=4"},"commit":{"message":"refactor: prefer contact (++) over hand crafting names","shortMessageHtmlLink":"refactor: prefer contact (++) over hand crafting names"}},{"before":null,"after":"f3bb9f0c4f97b19a6204693b31a20bc9a8e2e8e5","ref":"refs/heads/extract-rec-form-handling","pushedAt":"2024-08-16T09:55:11.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"Equilibris","name":"William Sørensen","path":"/Equilibris","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/47296141?s=80&v=4"},"commit":{"message":"refactor: extract handling of RecForms","shortMessageHtmlLink":"refactor: extract handling of RecForms"}},{"before":null,"after":"ab6aa44f27dcc67cf6e3bbd23aa66bd1b88a9c9d","ref":"refs/heads/generalize-constructor-generation-further","pushedAt":"2024-08-16T09:48:08.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"Equilibris","name":"William Sørensen","path":"/Equilibris","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/47296141?s=80&v=4"},"commit":{"message":"feat: generalize constructors further","shortMessageHtmlLink":"feat: generalize constructors further"}},{"before":null,"after":"3a2949ea63f21e2cca3c66ac33f68075e431b2fb","ref":"refs/heads/expose-curried-base","pushedAt":"2024-08-16T09:40:26.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"Equilibris","name":"William Sørensen","path":"/Equilibris","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/47296141?s=80&v=4"},"commit":{"message":"feat: add the ability to access the uncurried base","shortMessageHtmlLink":"feat: add the ability to access the uncurried base"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"djE6ks8AAAAEoWSJ2AA","startCursor":null,"endCursor":null}},"title":"Activity · alexkeizer/QpfTypes"}