{"push_id":3134547114,"size":2,"distinct_size":1,"ref":"refs/heads/master","head":"f962d2a88254a99bffbc7d0a40949872a80f4669","before":"fa9b7b19fc0409f3fdfa680e08f40a84594e8307","commits":[{"sha":"0b1ea03dafcf36880657ba910eec28ab78ccd018","author":{"name":"Georges Gonthier","email":"cf0bbf92c3bab544876275e917e4214bafe25822@inria.fr"},"message":"Adjust implicits of cancellation lemmas\n\nLike injectivity lemmas, instances of cancellation lemmas (whose\nconclusion is `cancel ? ?`, `{in ?, cancel ? ?}`, `pcancel`, or\n`ocancel`) are passed to\ngeneric lemmas such as `canRL` or `canLR_in`. Thus such lemmas should\nnot have trailing on-demand implicits _just before_ the `cancel`\nconclusion, as these would be inconvenient to insert (requiring\nessentially an explicit eta-expansion).\nWe therefore use `Arguments` or `Prenex Implicits` directives to make\nall such arguments maximally inserted implicits. We don’t, however make\nother arguments implicit, so as not to spoil direct instantiation of\nthe lemmas (in, e.g., `rewrite -[y](invmK injf)`).\nWe have also tried to do this with lemmas whose statement matches a\n`cancel`, i.e., ending in `forall x, g (E[x]) = x` (where pattern\nunification will pick up `f = fun x => E[x]`).\nWe also adjusted implicits of a few stray injectivity\nlemmas, and defined constants.\nWe provide a shorthand for reindexing a bigop with a permutation.\nFinally we used the new implicit signatures to simplify proofs that\nuse injectivity or cancellation lemmas.","distinct":false,"url":"https://api.github.com/repos/math-comp/math-comp/commits/0b1ea03dafcf36880657ba910eec28ab78ccd018"},{"sha":"f962d2a88254a99bffbc7d0a40949872a80f4669","author":{"name":"Cyril Cohen","email":"83060afa7e1c5e092e40b809eee653b9f20a485d@users.noreply.github.com"},"message":"Merge pull request #262 from math-comp/cancel-lemmas-implicit\n\nCancel lemmas implicit","distinct":true,"url":"https://api.github.com/repos/math-comp/math-comp/commits/f962d2a88254a99bffbc7d0a40949872a80f4669"}]}
{"actor":{"display_login":"CohenCyril"}}