sigma-andex
Switch to visible type applications
I noticed the documentation comments are not updated, they still show proxy syntax. I might change them later if i have time.
Another question that pops up for me is, now that the type signatures are shorter because they don't have a proxy in them, maybe we could have them directly in the functions, instead of an alias you have to look up? Maybe we could add some other, more general shortcuts: For example, we could have
index :: forall @m n elem. NonNegative m => NonNegative n => Compare m n LT => vect n elem -> elem
instead of
index :: forall @m n elem. Common.Index Vect m n elem.
A bit longer, but more readable and understandable at a glance, in my opinion. This is just an idea, would love to hear thoughts on it.
Yeah I was thinking the same. Somehow the type aliases are a bit annoying, but on the other hand, it would be a lot of (error-prone) copy-paste....