William J. Bowman
William J. Bowman
I could see an argument for yes. It would increase performance, and we ought to only be constructing well-typed terms. However, it might also be useful for debugging tactics.
I'd probably want both. I'm working through my demo, and after I define `#%datum` for the naturals, I type `0` in the REPL and `(z)` get printed. This is .....
Sure, started list above.
Sure if you want to do it :)
Known bug but I won't fix until the turnstile implementation is merged, which involves a documentation rewrite. Also, you probably want to install "turnstile-core" branch. -- Sent from my phoneamajig...
I'm not really sure what the right solution to this is yet. I think the new pattern expander supporting the old would be helpful, though. I think Coq's behavior is...
Don't remember; @pwang347, did you implement a particular algorithm? My guess would be it's ad-hoc, as the framework supports deep pattern matching and other things.
The library could extend `#%app` too, right?
Yeah, but then we could make a choice about whether to include it in the "core" to avoid diamond problems or not. In general, I want the code to enable...
How's this http://pkg-build.racket-lang.org/doc/cur@cur/Curnel_Forms.html#(form._((lib._cur/main..rkt)._elim))