agda-stdlib icon indicating copy to clipboard operation
agda-stdlib copied to clipboard

Published 20 hours ago • verified publisher icon agda

[ re #952, #356, #939, #1530 ] Overhaul of Functor/Applicative/Monad

Open gallais opened this issue 2 years ago • 2 comments

TODO:

  • [ ] CHANGELOG
  • [x] #1530

gallais avatar Oct 03 '22 20:10 gallais

Wow, that's impressive. That does indeed seem like quite the slog.

JacquesCarette avatar Oct 03 '22 21:10 JacquesCarette

Oof, finally writing a test case and I'm in level-hell because of IO. I'm experimenting with polymorphising but it is tempting to use an escape hatch to force IO : Set a -> Set a.

gallais avatar Oct 05 '22 21:10 gallais

Alright, I think this is approaching readiness. Sorry about the 3k+ LoC diff. :weary:

gallais avatar Oct 10 '22 21:10 gallais

Looks amazing @gallais. Thanks so much! Had a read through it and can't spot anything major to comment on.

MatthewDaggitt avatar Oct 20 '22 01:10 MatthewDaggitt