search

edwinb / Idris2-boot

A dependently typed programming language, a successor to Idris
https://idris-lang.org/
Other
902 stars 58 forks source link

Add equality functions for Vectors of potentially different lengths. #272

Closed jfdm closed 4 years ago

jfdm commented 4 years ago

Sized lists are useful, however, interfaces require that the length value is fixed. The added functions allow for vectors of potentually different lengths to be compared.

jfdm commented 4 years ago

Obviously something has changed since I wrote this, as the tests are failing. I will reopen once I have addressed the impact.