Why on Earth not
Conversation
You get annoying ambiguities with the dependent function syntax - ie. `(A : Set) -> A` - is this a non-dependent function from `A -> A` with the first `A` annotated, or is it a dependent function with a parameter named `A`?
2
1
1
For now in github.com/brendanzab/rus I've decided to use a keyword to disambiguate it `Fun (A : Type) -> A` - still not super happy though. 😰