cur
cur copied to clipboard
wilbowma
A less devious proof assistant
I think this is because we implement define with a variable transformer instead of actually expanding to a variable de-reference. It surprised me in my attempt at a staged programming...
watching an ML talk; they did something similar to improve module errors. For the large type errors, this might be helpful.
Predictable Macros for Hindley-Milner (Extended Abstract) TyDe 2020 github.com/gelisam/klister This would involve non-trivial extensions to the underlying macro system to do properly, but it looks like there are some good...
It looks like some types, namely universes (surprise surprise) are not fully expanded when they are matched against their pattern expanders. I'm guessing this happens because universes store their types...
``` #lang cur (require (only-in cur [new-elim elim])) (define-datatype Nat : Type (z : Nat) (s : (-> Nat Nat))) (begin-for-syntax (displayln (cur-reflect (cur-expand #`(lambda (x : Nat) (elim x...
The following ought to type check, since there are no other constructors whose type (index) matches the input type: ``` #lang cur (define-datatype Nat : Type (z : Nat) (s...
see examples in http://docs.racket-lang.org/cur/Curnel_Forms.html This is due automatically exporting types. Instead, I should make a require/provide transformer that exports the types only when a definition is required/provided.
``` raco test: "/home/root//user/.racket/7.7/pkgs/cur-test/cur/tests/ntac/software-foundations/Basics-ML.rkt" raco test: "/home/root//user/.racket/7.7/pkgs/cur-test/cur/tests/ntac/software-foundations/Basics.rkt" Racket virtual machine has run out of memory; aborting Aborted (core dumped) ``` We know of a few performance issues, e.g. lack of...
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?