search

statebox / idris-ct

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

Verified monads #42

Closed marcosh closed 5 years ago

marcosh commented 5 years ago

@clayrat could you please take a quick look? especially at the postulates I'm introducting

clayrat commented 5 years ago

@marcosh I rewrote VerifiedMonadAsMonad in a more idiomatic way and pushed it directly to this branch, seemed like a faster way, hope you don't mind?

marcosh commented 5 years ago

@clayrat not at all, thanks for it!