search

statebox / idris-ct

formally verified category theory library
GNU Affero General Public License v3.0
255 stars 23 forks source link

Pair as product in Idris #77

Closed Jake-Gillberg closed 4 years ago

Jake-Gillberg commented 4 years ago

Added a concrete implementation of Pair as Product in Idris, (similar to Either as CoProduct).

EitherAsCoProduct.lidr was missing access public export and default total directives, so I added those as well.

Jake-Gillberg commented 4 years ago

also, still quite new to idris and this library, so please let me know if I could make anything cleaner or more idiomatic!

clayrat commented 4 years ago

I think sticking to camelCase everywhere would make it a tiny bit more idiomatic ;)

Jake-Gillberg commented 4 years ago

I think sticking to camelCase everywhere would make it a tiny bit more idiomatic ;)

looking at the names of things in Coq got my head twisted :)

marcosh commented 4 years ago

Thanks @Jake-Gillberg, I merged it manually after removing some useless arguments (also from EitherAsCoProduct)