Thinking about dependently typed languages has brought back another question: Can you just state the associativity of append on length indexed lists in #Idris or #Agda?

Because Coq you can't because a type mismatch: (a + (b + c)) is not convertible to ((a + b) + c).

That seems to be a pretty annoying problem for the usability of dependently typed languages.

Because Coq you can't because a type mismatch: (a + (b + c)) is not convertible to ((a + b) + c).

That seems to be a pretty annoying problem for the usability of dependently typed languages.

Follow

Coq, associativity of vectors

lyxia@lyxia@niu.moeCoq, associativity of vectors

@amiloradovsky @turion @abs

In Coq it's called JMeq.