Stephen Chang
Stephen Chang
This is a temporary fix but it got me thinking, should we disable type checking completely while running tactics? The final term will be type checked anyways right?
run `ntac/trace` with this example (from here: https://github.com/wilbowma/cur/issues/121) ``` (ntac/trace (∀ (T : Type) (Σ (lst : (List T)) (And (== (List T) lst (nil T)) (Not (== (List T)...
UPDATE: This description is no longer true. See next comment. Not sure if anything can be done about this, but I thought it was interesting behavior. Using emacs `M-x uncomment`...
Currently, development in racketscript is somewhat painful, partially due to slow compile times (notes from discussion with @gamburgm) Many of the problems are already known or suspected (e.g., see https://github.com/racketscript/racketscript/issues/14...
Jotting down some notes from discussion with @gamburgm RacketScript runtime throws exceptions in different ways right now: - throw JS exceptions directly - e.g., https://github.com/racketscript/racketscript/blob/c1f802a9f2aec65b7f20bcaa9cf34abf62685b15/racketscript-compiler/racketscript/compiler/runtime/core/struct.js#L173 - everything using `check.js` (kernel...
`big-bang` missing handlers (according to [big-bang docs](https://docs.racket-lang.org/teachpack/2htdpuniverse.html#%28form._world._%28%28lib._2htdp%2Funiverse..rkt%29._big-bang%29%29)) - [ ] `name` `big-bang` handlers not completely working - [x] #303 - [x] #304 `htdp/image` missing features - [ ] https://github.com/racketscript/racketscript/issues/334