shuhung
shuhung
Is this ready to be merged?
The build failure is due to racket/racket@08bbc54f and is fixed in racket/racket@8eb5caee.
Hmm, could setting things to `#f` be a reaction to loading code from an unsaved buffer? I thought `.rkt` modules on the disk, before they are declared/expanded/instantiated, would be loaded...
> Maybe `current-load-relative-directory` should be set only during the expansion of the definitions window (as opposed to set and left alone even after expansion completes)? That would seem to be...
This improvement is awesome! In the long term, it'd be great if it's possible to prioritize this new lemma over the existing `≈-cong`, perhaps taking up its name and giving...
If I got it right, it looks like the framed thingy is an `editor%` snip here. https://github.com/racket/htdp/blob/8037f1cc620ed91fe68362ce5ad3d887269eb725/htdp-lib/test-engine/markup-gui.rkt#L145-L152 Is it possible for the copy behavior of the snip be changed to...
I think providing proofs of `eq`s in the lemmas is going to be a nice improvement. When I originally added some of the `cast` proofs, I did not think that...
Naming the revised lemmas with primes (like `∷ʳ-++′`) is quite inconvenient. Are they going to just replace the old ones in some major version (like v3.0)?
@MatthewDaggitt A good thing is that the exact equality here doesn't block any other equalities due to `eq`s being irrelevant in `cast`. That is, it's okay for the equality-specialized lemmas...
Rebasing to racket/racket@3c14248 should include the fix for the foreign test