{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":804477996,"defaultBranch":"main","name":"Idris2","ownerLogin":"troiganto","currentUserCanPush":false,"isFork":true,"isEmpty":false,"createdAt":"2024-05-22T17:00:23.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/5731814?v=4","public":true,"private":false,"isOrgOwned":false},"refInfo":{"name":"","listCacheKey":"v0:1717592277.0","currentOid":""},"activityList":{"items":[{"before":"ddc32c04659937b66b9e7b399fc7d76535643acd","after":"9ea2833911b071178dab123f79474c7cf5e036f0","ref":"refs/heads/drop-elem","pushedAt":"2024-06-05T13:07:44.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"troiganto","name":"Übertreiber","path":"/troiganto","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5731814?s=80&v=4"},"commit":{"message":"fix(base): runtime-erase implicit length argument to Vect's `dropElem`.\n\nThis makes it possible to call the function in more situations. It also\nbrings its signature in line with the overloads on `List`, `List1` and\n`SnocList`.\n\nThe previous implementation of `Data.Vect.Elem.dropElem` required the\nlength of the `Vect` to be available at runtime. This was used in order\nto recurse in the case that the `Elem` is not `Here`. However, it turns\nout that this is not actually necessary. Idris can deduce that the tail\nmust be non-empty if it contains an `Elem`.","shortMessageHtmlLink":"fix(base): runtime-erase implicit length argument to Vect's <code>dropElem</code>."}},{"before":"d56accd8498d76a340f7b2481deebe8231c833c2","after":"ddc32c04659937b66b9e7b399fc7d76535643acd","ref":"refs/heads/drop-elem","pushedAt":"2024-06-05T13:05:03.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"troiganto","name":"Übertreiber","path":"/troiganto","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5731814?s=80&v=4"},"commit":{"message":"fix(base): runtime-erase implicit length argument to `dropElem`.\n\nThis makes it possible to call the function in more situations.\n\nThe previous implementation of `Data.Vect.Elem.dropElem` required the\nlength of the `Vect` to be available at runtime. This was used in order\nto recurse in the case that the `Elem` is not `Here`.\n\nHowever, it turns out that this is not actually necessary. Idris can\ndeduce that the tail must be non-empty if it contains an `Elem`.","shortMessageHtmlLink":"fix(base): runtime-erase implicit length argument to <code>dropElem</code>."}},{"before":"ad4697da447044babc33305af8ccceef9cd79ea5","after":null,"ref":"refs/heads/nub-by","pushedAt":"2024-06-05T12:57:57.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"troiganto","name":"Übertreiber","path":"/troiganto","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5731814?s=80&v=4"}},{"before":"cf68e995c414912c338ae694a74fd833a6c4cee2","after":"2c128e216c367c1e76d5445962d6bb316c93d4e9","ref":"refs/heads/main","pushedAt":"2024-06-05T12:57:04.000Z","pushType":"push","commitsCount":16,"pusher":{"login":"troiganto","name":"Übertreiber","path":"/troiganto","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5731814?s=80&v=4"},"commit":{"message":"refactor(base): move implementation of `Data.Vect.nubBy` to global scope\n\nCloses #3285","shortMessageHtmlLink":"refactor(base): move implementation of <code>Data.Vect.nubBy</code> to global scope"}},{"before":"34bf6f2573c75578c5277b2835859cd2cea48866","after":"d56accd8498d76a340f7b2481deebe8231c833c2","ref":"refs/heads/drop-elem","pushedAt":"2024-05-23T15:21:33.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"troiganto","name":"Übertreiber","path":"/troiganto","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5731814?s=80&v=4"},"commit":{"message":"fix(base): runtime erase implicit length argument to dropElem\n\nThe previous implementation of `Data.Vect.Elem.dropElem` required the\nlength of the `Vect` to be available at runtime. This was used in order\nto recurse in the case that the `Elem` is not `Here`.\n\nHowever, it turns out that this is not actually necessary. Idris can\ndeduce that the tail must be non-empty if it contains an `Elem`.","shortMessageHtmlLink":"fix(base): runtime erase implicit length argument to dropElem"}},{"before":"86dcd4451d4c5f565733f01b73542cb43c70494e","after":"ad4697da447044babc33305af8ccceef9cd79ea5","ref":"refs/heads/nub-by","pushedAt":"2024-05-23T15:21:02.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"troiganto","name":"Übertreiber","path":"/troiganto","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5731814?s=80&v=4"},"commit":{"message":"refactor(base): move implementation of `Data.Vect.nubBy` to global scope\n\nCloses #3285","shortMessageHtmlLink":"refactor(base): move implementation of <code>Data.Vect.nubBy</code> to global scope"}},{"before":"1ddfe8cbd3352b751e271da8da6efc2dad4128e3","after":"34bf6f2573c75578c5277b2835859cd2cea48866","ref":"refs/heads/drop-elem","pushedAt":"2024-05-23T15:20:19.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"troiganto","name":"Übertreiber","path":"/troiganto","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5731814?s=80&v=4"},"commit":{"message":"fix(base): runtime erase implicit length argument to dropElem\n\nThe previous implementation of `Data.Vect.Elem.dropElem` required the\nlength of the `Vect` to be available at runtime. This was used in order\nto recurse in the case that the `Elem` is not `Here`.\n\nHowever, it turns out that this is not actually necessary. Idris can\ndeduce that the tail must be non-empty if it contains an `Elem`.","shortMessageHtmlLink":"fix(base): runtime erase implicit length argument to dropElem"}},{"before":"5d44aaa4536471cb7b552fda3f16b44168e044b9","after":"86dcd4451d4c5f565733f01b73542cb43c70494e","ref":"refs/heads/nub-by","pushedAt":"2024-05-23T15:16:27.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"troiganto","name":"Übertreiber","path":"/troiganto","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5731814?s=80&v=4"},"commit":{"message":"refactor(base): move implementation of `Data.Vect.nubBy` to global scope\n\nCloses #3285","shortMessageHtmlLink":"refactor(base): move implementation of <code>Data.Vect.nubBy</code> to global scope"}},{"before":null,"after":"1ddfe8cbd3352b751e271da8da6efc2dad4128e3","ref":"refs/heads/drop-elem","pushedAt":"2024-05-23T15:11:54.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"troiganto","name":"Übertreiber","path":"/troiganto","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5731814?s=80&v=4"},"commit":{"message":"fix(base): runtime erase implicit length argument to dropElem\n\nThe previous implementation of `Data.Vect.Elem.dropElem` required the\nlength of the `Vect` to be available at runtime. This was used in order\nto recurse in the case that the `Elem` is not `Here`.\n\nHowever, it turns out that this is not actually necessary. Idris can\ndeduce that the tail must be non-empty if it contains an `Elem`.","shortMessageHtmlLink":"fix(base): runtime erase implicit length argument to dropElem"}},{"before":null,"after":"5d44aaa4536471cb7b552fda3f16b44168e044b9","ref":"refs/heads/nub-by","pushedAt":"2024-05-23T15:02:02.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"troiganto","name":"Übertreiber","path":"/troiganto","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/5731814?s=80&v=4"},"commit":{"message":"refactor(base): move implementation of `Data.Vect.nubBy` to global scope\n\nCloses #3285","shortMessageHtmlLink":"refactor(base): move implementation of <code>Data.Vect.nubBy</code> to global scope"}}],"hasNextPage":false,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"djE6ks8AAAAEXSJ9IQA","startCursor":null,"endCursor":null}},"title":"Activity · troiganto/Idris2"}