Jeremy G. Siek
Jeremy G. Siek
The name in the literature for self-typed things (i.e. a type inhabited by exactly one value) is "singleton types". I'd be hesitant to use singleton types for number literals because...
Great! BTW, here's the code that I cobbled together for the time being: ``` #lang racket (require graph) (provide (all-defined-out)) (define (remove-all v lst) (cond [(null? lst) lst] [(equal? v...
Good question. Yes, I'm using `tsort`.
Just to be clear, the intent here is to remove the need for `observe` declarations for type equality. This question-for-leads does not apply to other kinds of `observe` declarations, such...
It would be helpful to see an example of how this would change the proofs that currently use the congruence rules, such as the proof of `rename-subst-ren`.
Which Chapters of PLFA would these proposed changes impact?
Instead of `DeBruijn`, it looks like `Untyped` would need to change. But then there's the question of whether we'd want to let these chapters be slightly out of sync with...
I'm OK with this change as long as it doesn't break any of the uses of it, or as long as your PR fixes any downstream uses.
This issue with repeated fnty a good observation. Certainly a disadvantage of the current syntax.
Thanks for noticing this! I've made a pull request to fix it.