{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":76963442,"defaultBranch":"master","name":"math-comp","ownerLogin":"ybertot","currentUserCanPush":false,"isFork":true,"isEmpty":false,"createdAt":"2016-12-20T14:30:00.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/3407333?v=4","public":true,"private":false,"isOrgOwned":false},"refInfo":{"name":"","listCacheKey":"v0:1716816639.0","currentOid":""},"activityList":{"items":[{"before":null,"after":"5d8331f4174ba53ec823a40440574afa4eb2a11a","ref":"refs/heads/sorted_cat_rcons-mc1","pushedAt":"2024-05-27T13:30:39.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"ybertot","name":"Yves Bertot","path":"/ybertot","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3407333?s=80&v=4"},"commit":{"message":"Adds a lemma to reason by equivalence on paths cut in the middle\ngeneralization of cat_path, but accepts the case where the prefix could\nbe empty (requires a proof by cases)","shortMessageHtmlLink":"Adds a lemma to reason by equivalence on paths cut in the middle"}},{"before":"d06325d2e5957546bd70871ede4b33d0901d3be1","after":"7a4e882945ee7de1cce72e72e890629d6acabf37","ref":"refs/heads/sorted_cat_rcons","pushedAt":"2024-05-27T08:37:01.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"ybertot","name":"Yves Bertot","path":"/ybertot","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3407333?s=80&v=4"},"commit":{"message":"Adds a lemma to reason by equivalence on paths cut in the middle\ngeneralization of cat_path, but accepts the case where the prefix could\nbe empty (requires a proof by cases)","shortMessageHtmlLink":"Adds a lemma to reason by equivalence on paths cut in the middle"}},{"before":"040af03b9bc6c1cee6a17796538eb9742ffd737a","after":"d06325d2e5957546bd70871ede4b33d0901d3be1","ref":"refs/heads/sorted_cat_rcons","pushedAt":"2024-05-22T06:37:40.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"ybertot","name":"Yves Bertot","path":"/ybertot","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3407333?s=80&v=4"},"commit":{"message":"Adds a lemma to reason by equivalence on paths cut in the middle\ngeneralization of cat_path, but accepts the case where the prefix could\nbe empty (requires a proof by cases)","shortMessageHtmlLink":"Adds a lemma to reason by equivalence on paths cut in the middle"}},{"before":null,"after":"040af03b9bc6c1cee6a17796538eb9742ffd737a","ref":"refs/heads/sorted_cat_rcons","pushedAt":"2024-05-22T06:20:49.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"ybertot","name":"Yves Bertot","path":"/ybertot","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3407333?s=80&v=4"},"commit":{"message":"Adds a lemma to reason by equivalence on paths cut in the middle\ngeneralization of cat_path, but accepts the case where the prefix could\nbe empty (requires a proof by cases)","shortMessageHtmlLink":"Adds a lemma to reason by equivalence on paths cut in the middle"}},{"before":"5a64ea4f5cd52d1818c5782d6c4bb188866c3410","after":"a9b068b86a3d16d16325828a8f4b11cf0ea401bd","ref":"refs/heads/solve_Qint_span","pushedAt":"2024-03-29T14:07:40.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"ybertot","name":"Yves Bertot","path":"/ybertot","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3407333?s=80&v=4"},"commit":{"message":"space twiddling","shortMessageHtmlLink":"space twiddling"}},{"before":null,"after":"5a64ea4f5cd52d1818c5782d6c4bb188866c3410","ref":"refs/heads/solve_Qint_span","pushedAt":"2024-03-29T13:51:21.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"ybertot","name":"Yves Bertot","path":"/ybertot","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3407333?s=80&v=4"},"commit":{"message":"removes a usage of the subst tactic, relying on idiomatic ssreflect","shortMessageHtmlLink":"removes a usage of the subst tactic, relying on idiomatic ssreflect"}}],"hasNextPage":false,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"djE6ks8AAAAEVO48vgA","startCursor":null,"endCursor":null}},"title":"Activity · ybertot/math-comp"}