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.

Coq, associativity of vectors 

Coq, associativity of vectors 

Coq, associativity of vectors 

Follow

Coq, associativity of vectors 

Coq, associativity of vectors 

Coq, concatenation of vectors 

Coq, concatenation of vectors 

Coq, concatenation of vectors 

Coq, concatenation of vectors 

re: Coq, associativity of vectors 

re: Coq, associativity of vectors 

Sign in to participate in the conversation
niu.moe

Welcome to your niu world ! We are a cute and loving international community O(≧▽≦)O !