Proper Treatment 正當作法/ blog/ posts/ Dependent equality/ discussion 討論
2010-10-22 05:02

I am afraid that the only way to simplify is to not use the type “vector”, i.e. a list should not have its length in its type. Just use traditional lists, when you prove something about a length, use the “length” function.