{"push_id":1049113058,"size":4,"distinct_size":4,"ref":"refs/heads/master","head":"ab385cd72b158bc05a01b6a8b16e77a9d3aa288d","before":"33a08b90084b25cb6e41a847903d9e87ac82bfbc","commits":[{"sha":"b92f7acadf02efcfa020a9f4601e55cb96548aa4","author":{"email":"435e2a4f8ba8cc6bf7a8685499cd59003323ddf3@st-andrews.ac.uk","name":"Edwin Brady"},"message":"New implementation of rewrite\n\nNot using the 'rewrite' tactic any more, but building an application of\na rewriting lemma with a predicate directly. This allows a new syntax:\n\nrewrite [rule] using [rewrite_lemma] in [scope]\n\nWhere rewrite_lemma is any function of the right shape, so can be a\nfunction used to rewrite dependent types rather than the default, which\nis rewrite__impl.\n\nMore to do: the rewrite_lemma could be generated automatically for many\ndependent types, also the predicate building needs a bit of polish, but\nthis already works for, e.g., rewriting vector functions.","distinct":true,"url":"https://api.github.com/repos/idris-lang/Idris-dev/commits/b92f7acadf02efcfa020a9f4601e55cb96548aa4"},{"sha":"b66865f89f97c7eae2bd304aa47363fc26ececdb","author":{"email":"435e2a4f8ba8cc6bf7a8685499cd59003323ddf3@st-andrews.ac.uk","name":"Edwin Brady"},"message":"Reinstate checking of rewrite result type","distinct":true,"url":"https://api.github.com/repos/idris-lang/Idris-dev/commits/b66865f89f97c7eae2bd304aa47363fc26ececdb"},{"sha":"40182da30b6e1d1ab7843adf082d222066e7c417","author":{"email":"435e2a4f8ba8cc6bf7a8685499cd59003323ddf3@st-andrews.ac.uk","name":"Edwin Brady"},"message":"Modify the way of finding rewriting lemma","distinct":true,"url":"https://api.github.com/repos/idris-lang/Idris-dev/commits/40182da30b6e1d1ab7843adf082d222066e7c417"},{"sha":"ab385cd72b158bc05a01b6a8b16e77a9d3aa288d","author":{"email":"435e2a4f8ba8cc6bf7a8685499cd59003323ddf3@st-andrews.ac.uk","name":"Edwin Brady"},"message":"Generate rewriting lemmas for data types\n\nIf no rewrite lemma is specified in a 'rewrite' construct, and one is\navailable for the types in the equality, apply that.\nRewriting lemmas may fail to generate in some cases (I haven't yet\nworked out exactly what the criteria are, and if we can fix it...) in\nwhich case it fails silently, at least until the rewrite is applied.\n\nThe result is that, for example, rewrites on equalities on vectors and\nother similar types can be applied without doing anything special.","distinct":true,"url":"https://api.github.com/repos/idris-lang/Idris-dev/commits/ab385cd72b158bc05a01b6a8b16e77a9d3aa288d"}]}