G. Allais
G. Allais
Merged on frex
I'd say that's a duplicate of #806
Note that this leads to a lot of normalisation (and may be missing some occurrences in the context thus leading to ill-typed auxiliary definitions).
Not sure. I have also observed it with the bright orange highlighting of declarations not accompanied by a definition: adding a stub does not make the colour go away. :/
AFAIK MLTT is currently a valid model of Idris 2 via quantities erasure. Adding anti-unifiability of pi types with different annotations on their domain would force all models to discriminate...
> Could we use the new abstract feature somehow to prevent reduction? This is what I was going to suggest we should experiment with. However the following does not typecheck...
Note that Agda also gives you access to these definitions as some sort of defined projections out of the record. ```agda open import Agda.Builtin.Nat record ANat : Set where constructor...
It's a feature of the way we desugar record declarations into modules of mutual definitions so I'd say the interpretation is pretty open-ended. I agree the current feature is useful...
Note that you get a pretty bad case tree because of `{a : Type} -> ...`. At the repl, `:di bad` gives us (I've cleaned up the tree that was...
That last one is properly rejected if you use `%default total`. The totality checker somehow forgets to check that `D` is positive despite being in `Omega`'s dependency graph. I've tried...