{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":202568092,"defaultBranch":"master","name":"bonak","ownerLogin":"artagnon","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2019-08-15T15:40:39.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/37226?v=4","public":true,"private":false,"isOrgOwned":false},"refInfo":{"name":"","listCacheKey":"v0:1716124890.0","currentOid":""},"activityList":{"items":[{"before":"7b62b060e62d47f892197fd05d726eb4e5f35235","after":"e1204e80e3eb0b475540b590cd5be72c611007a0","ref":"refs/heads/le-typeclass","pushedAt":"2024-06-30T21:57:48.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"herbelin","name":"Hugo Herbelin","path":"/herbelin","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/460771?s=80&v=4"},"commit":{"message":"A version of mkDgnPaintingType which works (abstracting over LiftDgn).","shortMessageHtmlLink":"A version of mkDgnPaintingType which works (abstracting over LiftDgn)."}},{"before":"2f2abfa60065ca35a62df90f07a8f3f1febf66fb","after":"7b62b060e62d47f892197fd05d726eb4e5f35235","ref":"refs/heads/le-typeclass","pushedAt":"2024-06-30T15:49:21.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"artagnon","name":"Ramkumar Ramachandra","path":"/artagnon","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/37226?s=80&v=4"},"commit":{"message":"Notation: clean up unused notation; squelch warning","shortMessageHtmlLink":"Notation: clean up unused notation; squelch warning"}},{"before":"7dbf3610a06a9b84776ecb231314ffbcd38627b3","after":"2f2abfa60065ca35a62df90f07a8f3f1febf66fb","ref":"refs/heads/le-typeclass","pushedAt":"2024-06-30T15:00:11.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"artagnon","name":"Ramkumar Ramachandra","path":"/artagnon","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/37226?s=80&v=4"},"commit":{"message":"mkDgnPainting: underlying problem","shortMessageHtmlLink":"mkDgnPainting: underlying problem"}},{"before":"1b218321f32de75cc7a5af81c4650add1a2ad5ed","after":"7dbf3610a06a9b84776ecb231314ffbcd38627b3","ref":"refs/heads/le-typeclass","pushedAt":"2024-06-30T14:21:28.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"herbelin","name":"Hugo Herbelin","path":"/herbelin","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/460771?s=80&v=4"},"commit":{"message":"Adding sigT_commute.","shortMessageHtmlLink":"Adding sigT_commute."}},{"before":"f96e5c1360b893ce3cba6a7c91edecf0bcd50d72","after":"1b218321f32de75cc7a5af81c4650add1a2ad5ed","ref":"refs/heads/le-typeclass","pushedAt":"2024-06-23T11:34:24.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"artagnon","name":"Ramkumar Ramachandra","path":"/artagnon","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/37226?s=80&v=4"},"commit":{"message":"mkCohDgnRestrLayer: finish","shortMessageHtmlLink":"mkCohDgnRestrLayer: finish"}},{"before":"b7e4bd656f37fe9cedb41c56340a55ca411a0f56","after":"f96e5c1360b893ce3cba6a7c91edecf0bcd50d72","ref":"refs/heads/le-typeclass","pushedAt":"2024-06-23T10:43:02.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"herbelin","name":"Hugo Herbelin","path":"/herbelin","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/460771?s=80&v=4"},"commit":{"message":"One step more","shortMessageHtmlLink":"One step more"}},{"before":"3107bd379ab06b62402076f0084d5b7bb2973bbc","after":"b7e4bd656f37fe9cedb41c56340a55ca411a0f56","ref":"refs/heads/le-typeclass","pushedAt":"2024-06-23T10:34:07.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"herbelin","name":"Hugo Herbelin","path":"/herbelin","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/460771?s=80&v=4"},"commit":{"message":"Implicit arg of cohDgnRestrFrame.","shortMessageHtmlLink":"Implicit arg of cohDgnRestrFrame."}},{"before":"09b38853fe253034c664b1595df6babb98548f6f","after":"3107bd379ab06b62402076f0084d5b7bb2973bbc","ref":"refs/heads/le-typeclass","pushedAt":"2024-06-02T13:52:04.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"herbelin","name":"Hugo Herbelin","path":"/herbelin","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/460771?s=80&v=4"},"commit":{"message":"First step in mkCohDgnRestrLayer","shortMessageHtmlLink":"First step in mkCohDgnRestrLayer"}},{"before":"1e6400b72ae81f9b292119b3edd3febafc61f767","after":"09b38853fe253034c664b1595df6babb98548f6f","ref":"refs/heads/le-typeclass","pushedAt":"2024-06-02T13:50:54.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"artagnon","name":"Ramkumar Ramachandra","path":"/artagnon","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/37226?s=80&v=4"},"commit":{"message":"fix some minor issues in new proofs","shortMessageHtmlLink":"fix some minor issues in new proofs"}},{"before":"642a6107e4e97464c89d5f4c6d5027a6ed977b79","after":"1e6400b72ae81f9b292119b3edd3febafc61f767","ref":"refs/heads/le-typeclass","pushedAt":"2024-06-02T13:42:43.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"artagnon","name":"Ramkumar Ramachandra","path":"/artagnon","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/37226?s=80&v=4"},"commit":{"message":"cohDgnRestrPainting: new statement","shortMessageHtmlLink":"cohDgnRestrPainting: new statement"}},{"before":"548c89235204addfaf52c5602a5e2bbef964f6ed","after":"642a6107e4e97464c89d5f4c6d5027a6ed977b79","ref":"refs/heads/le-typeclass","pushedAt":"2024-06-02T13:39:35.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"artagnon","name":"Ramkumar Ramachandra","path":"/artagnon","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/37226?s=80&v=4"},"commit":{"message":"mkDgnFrameBlock: finish!","shortMessageHtmlLink":"mkDgnFrameBlock: finish!"}},{"before":"6f1f1eec967b7b439694853acd75d5b620567b8a","after":"548c89235204addfaf52c5602a5e2bbef964f6ed","ref":"refs/heads/le-typeclass","pushedAt":"2024-06-02T12:42:41.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"artagnon","name":"Ramkumar Ramachandra","path":"/artagnon","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/37226?s=80&v=4"},"commit":{"message":"LeYoneda: gfail after anomaly; fix hang","shortMessageHtmlLink":"LeYoneda: gfail after anomaly; fix hang"}},{"before":"91025922645107bd6712d36416df49deb88bc63f","after":"6f1f1eec967b7b439694853acd75d5b620567b8a","ref":"refs/heads/le-typeclass","pushedAt":"2024-06-02T11:15:02.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"herbelin","name":"Hugo Herbelin","path":"/herbelin","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/460771?s=80&v=4"},"commit":{"message":"Abstracting over (C:νType n'.+1).","shortMessageHtmlLink":"Abstracting over (C:νType n'.+1)."}},{"before":"49614e5fd003cadf635af836bb3ea3fdd83781e7","after":"91025922645107bd6712d36416df49deb88bc63f","ref":"refs/heads/le-typeclass","pushedAt":"2024-05-27T09:21:58.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"artagnon","name":"Ramkumar Ramachandra","path":"/artagnon","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/37226?s=80&v=4"},"commit":{"message":"Speedup achieved via proof simplification","shortMessageHtmlLink":"Speedup achieved via proof simplification"}},{"before":"199a16c99b7657e7e05e434b57d33779fc7a01ac","after":"49614e5fd003cadf635af836bb3ea3fdd83781e7","ref":"refs/heads/le-typeclass","pushedAt":"2024-05-27T08:37:36.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"artagnon","name":"Ramkumar Ramachandra","path":"/artagnon","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/37226?s=80&v=4"},"commit":{"message":"NFC proof simplifications","shortMessageHtmlLink":"NFC proof simplifications"}},{"before":"60a7a56844b8893d18824d1d80001adb99e6d607","after":"199a16c99b7657e7e05e434b57d33779fc7a01ac","ref":"refs/heads/le-typeclass","pushedAt":"2024-05-27T08:31:51.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"artagnon","name":"Ramkumar Ramachandra","path":"/artagnon","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/37226?s=80&v=4"},"commit":{"message":"mkCohPainting_step: NFC simplification of proof","shortMessageHtmlLink":"mkCohPainting_step: NFC simplification of proof"}},{"before":"3b563cc3eefee8fe63f913210156b34569461c20","after":"60a7a56844b8893d18824d1d80001adb99e6d607","ref":"refs/heads/le-typeclass","pushedAt":"2024-05-26T15:57:27.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"artagnon","name":"Ramkumar Ramachandra","path":"/artagnon","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/37226?s=80&v=4"},"commit":{"message":"mkCohPaintingHyp: simplify implicit-explicit args","shortMessageHtmlLink":"mkCohPaintingHyp: simplify implicit-explicit args"}},{"before":"5cf734be674c3ed7ae583f226f6daa6edfaaf21d","after":"3b563cc3eefee8fe63f913210156b34569461c20","ref":"refs/heads/le-typeclass","pushedAt":"2024-05-26T15:44:39.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"artagnon","name":"Ramkumar Ramachandra","path":"/artagnon","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/37226?s=80&v=4"},"commit":{"message":"proof simplifications (NFC)","shortMessageHtmlLink":"proof simplifications (NFC)"}},{"before":"0dc1c5330e6b62817b8a1f34d2d5ed2797ebda40","after":"5cf734be674c3ed7ae583f226f6daa6edfaaf21d","ref":"refs/heads/le-typeclass","pushedAt":"2024-05-26T15:36:26.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"artagnon","name":"Ramkumar Ramachandra","path":"/artagnon","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/37226?s=80&v=4"},"commit":{"message":"mkLayer, mkLayer': make d explicit","shortMessageHtmlLink":"mkLayer, mkLayer': make d explicit"}},{"before":"d050b9b362f1220b4af7eded503d3af7ebc6768c","after":"0dc1c5330e6b62817b8a1f34d2d5ed2797ebda40","ref":"refs/heads/le-typeclass","pushedAt":"2024-05-26T13:10:05.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"artagnon","name":"Ramkumar Ramachandra","path":"/artagnon","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/37226?s=80&v=4"},"commit":{"message":"eqDgnFrameSp: a first attempt","shortMessageHtmlLink":"eqDgnFrameSp: a first attempt"}},{"before":"368aa3c0c3569420455b0b7ed2a385ed2a131cbd","after":"d050b9b362f1220b4af7eded503d3af7ebc6768c","ref":"refs/heads/le-typeclass","pushedAt":"2024-05-26T10:01:40.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"artagnon","name":"Ramkumar Ramachandra","path":"/artagnon","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/37226?s=80&v=4"},"commit":{"message":"Dgn: factor out more inequalities","shortMessageHtmlLink":"Dgn: factor out more inequalities"}},{"before":"558953a8c786c0eca1e3417df60f8a2f6f4080c4","after":"368aa3c0c3569420455b0b7ed2a385ed2a131cbd","ref":"refs/heads/le-typeclass","pushedAt":"2024-05-26T09:38:53.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"artagnon","name":"Ramkumar Ramachandra","path":"/artagnon","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/37226?s=80&v=4"},"commit":{"message":"LeYoenda: fix hang in decision tactic","shortMessageHtmlLink":"LeYoenda: fix hang in decision tactic"}},{"before":"3a8ff71ce696772de883601e252ac6fb3e55c455","after":"558953a8c786c0eca1e3417df60f8a2f6f4080c4","ref":"refs/heads/le-typeclass","pushedAt":"2024-05-25T14:45:07.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"artagnon","name":"Ramkumar Ramachandra","path":"/artagnon","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/37226?s=80&v=4"},"commit":{"message":"LeYoneda: consolidate is_less (NFC)","shortMessageHtmlLink":"LeYoneda: consolidate is_less (NFC)"}},{"before":"899f9d778f779d1bdb7459973fbfa3eaed6973d4","after":"3a8ff71ce696772de883601e252ac6fb3e55c455","ref":"refs/heads/le-typeclass","pushedAt":"2024-05-25T13:27:01.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"artagnon","name":"Ramkumar Ramachandra","path":"/artagnon","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/37226?s=80&v=4"},"commit":{"message":"LeYoneda: refactor decision tactic; add hang example","shortMessageHtmlLink":"LeYoneda: refactor decision tactic; add hang example"}},{"before":"e37885afa0452093d01ea3b49c6737a1b17d850a","after":"899f9d778f779d1bdb7459973fbfa3eaed6973d4","ref":"refs/heads/le-typeclass","pushedAt":"2024-05-19T23:07:04.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"artagnon","name":"Ramkumar Ramachandra","path":"/artagnon","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/37226?s=80&v=4"},"commit":{"message":"Just Dgn records left","shortMessageHtmlLink":"Just Dgn records left"}},{"before":"14da22da374203ff04bda1c16a1d3d48fa144110","after":"e37885afa0452093d01ea3b49c6737a1b17d850a","ref":"refs/heads/le-typeclass","pushedAt":"2024-05-19T22:12:49.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"artagnon","name":"Ramkumar Ramachandra","path":"/artagnon","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/37226?s=80&v=4"},"commit":{"message":"restrPainting: factor out inequalities","shortMessageHtmlLink":"restrPainting: factor out inequalities"}},{"before":"019bca0042569a0cc1f04e2e4e8131078b7feeec","after":"14da22da374203ff04bda1c16a1d3d48fa144110","ref":"refs/heads/le-typeclass","pushedAt":"2024-05-19T21:14:56.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"artagnon","name":"Ramkumar Ramachandra","path":"/artagnon","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/37226?s=80&v=4"},"commit":{"message":"cohFrame: factor out inequalities","shortMessageHtmlLink":"cohFrame: factor out inequalities"}},{"before":"097554d7504bcfc5a66c2f8684df5ae1740d4c44","after":"019bca0042569a0cc1f04e2e4e8131078b7feeec","ref":"refs/heads/le-typeclass","pushedAt":"2024-05-19T17:30:03.000Z","pushType":"push","commitsCount":2,"pusher":{"login":"artagnon","name":"Ramkumar Ramachandra","path":"/artagnon","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/37226?s=80&v=4"},"commit":{"message":"cohFrame: figure out p, q, r in some cases","shortMessageHtmlLink":"cohFrame: figure out p, q, r in some cases"}},{"before":"656f7ecec3ebac26abb76715ff39e38a3c7515cd","after":"097554d7504bcfc5a66c2f8684df5ae1740d4c44","ref":"refs/heads/le-typeclass","pushedAt":"2024-05-19T16:32:55.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"artagnon","name":"Ramkumar Ramachandra","path":"/artagnon","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/37226?s=80&v=4"},"commit":{"message":"simplify some proofs; factor out changing inequalities","shortMessageHtmlLink":"simplify some proofs; factor out changing inequalities"}},{"before":"d449380c1387339cf7932529043ee389fd672859","after":"656f7ecec3ebac26abb76715ff39e38a3c7515cd","ref":"refs/heads/le-typeclass","pushedAt":"2024-05-19T16:25:25.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"artagnon","name":"Ramkumar Ramachandra","path":"/artagnon","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/37226?s=80&v=4"},"commit":{"message":"frame', mkRestrLayer: factor out inequalities","shortMessageHtmlLink":"frame', mkRestrLayer: factor out inequalities"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"djE6ks8AAAAEcy7ynwA","startCursor":null,"endCursor":null}},"title":"Activity · artagnon/bonak"}