Stephen Chang
Stephen Chang
Yes, it's a problem. We can't get rid of the `variable-transformer` (because then ids wont have types), but `define` in `coc.rkt` should be using the expanded `e`. It doesnt right...
dupe of https://github.com/wilbowma/cur/issues/37 and https://github.com/wilbowma/cur/issues/90?
yeah i agree. just remembered it was missing and couldnt find an issue for it
Yes this is a known problem. If you look at `current-typecheck-relation` it has to check for both unexpanded and unexpanded `Type` too. So your hack is reasonable. Not sure how...
solving https://github.com/wilbowma/cur/issues/90 (or https://github.com/wilbowma/cur/issues/37) would also help with this?
Yes, right now a term expanded from a general `elim` is indistinguishable from a type specific one. Same with expanded lambda, it doesnt know if the original term had an...
so this is a doc issue?
Is this new? Or has it always been doing this
fixes #121
True. I do see that several tactics raise their own exceptions when given an ill-typed expression, so it may not be completely straightforward to completely disable type checking. For now,...