William J. Bowman
William J. Bowman
Thanks! I just cut that part of the demo. I can do with out it.
I wouldn't say dupe, but it is related. #37 and #90 are dupes. I consider that related to implementing things like Coq's `cbn` and `cbv` tactics, which let the user...
Partially addressed, but the issue is we need lazy (by-need) \delta-reduction, I think.
https://docs.racket-lang.org/sexp-diff/index.html#%28def._%28%28lib._sexp-diff%2Fmain..rkt%29._stx-diff%29%29
https://www.youtube.com/watch?v=n3eS-yuSJ_U
I don't know how to do this locally. The algorithm Coq uses is a module-level constraint solver, which I disapprove of :(
You'll need to pull/reset on master (we finally merged everything!). I "fixed" that bug. That sounds about right. I don't see the potential performance issue though. I'd probably try to...
Yes, you'll need to update to Turnstile's main branch. You can probably do this by uninstalling turnstile etc, then just do `raco pkg install` from `cur-lib` and it will pull...
I think it was both a doc and REPL issue. I know the REPL part has been fixed as I've been exercising that during my demo. Not sure about the...
Not sure. Only just noticed. -- Sent from my phoneamajig > On Jun 18, 2020, at 18:14, Stephen Chang wrote: > > > Is this new? Or has it...