Jason Gross
Jason Gross
Of the time spent in the new rewrite rule reification, 82.7% is spent in [`replace_type_try_transport`](https://github.com/mit-plv/rewriter/blob/03889802d6ddb8dcaeb922206f07c3836d0a7b49/src/Rewriter/Rewriter/Reify.v#L597-L636) (236.006s max for a single call), which is basically "`match context[@type.try_transport ?base_type ?try_make_transport_base_type_cps ?p ?t...
Currently, we cannot handle rewrite rules such as ```coq forall x, '(S x) = pred '(S (S x)) ``` because we end up generating a pattern like `forall x1 x2,...
It's quite painful to figure out why rewriter rules aren't matching. It should be possible, using a combination of [reduction-effects](https://github.com/coq-community/reduction-effects) for `cbv` (alas, no support for `native_compute` / `vm_compute`, yet;...
I don't think the rewriter is suitable for wider adoption. It's very, very, very much a research prototype, and I don't see it becoming not a research prototype without going...
The file https://github.com/mit-plv/rewriter/blob/master/src/Rewriter/Demo.v should be fleshed out and completed. Perhaps ideally in time for the POPL submission.
> I presented Delta at [CodeCon 2006](http://www.codecon.org/2006/). The slides are [here](https://github.com/dsw/delta/blob/master/delta_codecon.ppt). Both of these links are 404s. (Context is that I'm trying to figure out what to cite for an...
Generated by [rubber](https://tex-talk.net/2011/12/building-documents-with-rubber/). [The docs](https://github.com/petrhosek/rubber/blob/8ec18fd096b186901f197d26c8e1060b42f0b34f/doc/rubber.texi#L158) claim to use `rubber.cache`, but I've seen $filename.rubbercache in the wild, so I'm including both. **Reasons for making this change:** _TODO_ **Links to documentation supporting...
It would be nice to support well-typed-by-construction expression types, such as [nested abstract syntax](https://math.unice.fr/~ah/div/fsubwf.pdf) where we have `expr : Type -> Type`, we label both variables in `expr V` with...
#### Description of the problem One would think that `Scheme Case` would generate the same sort of lemma as [`Set Case Analysis Schemes`](https://coq.inria.fr/refman/user-extensions/proof-schemes.html#coq:flag.case-analysis-schemes), but instead it seems to generate a...
```coq Require Ltac2.Ltac2. Require Import Ltac2.Init Ltac2.Control Ltac2.Notations. Goal (fun (x : nat) => let y := x in fun x : nat => y + x) = (fun x...