search

jonsterling / agda-calf

A cost-aware logical framework, embedded in Agda.
https://jonsterling.github.io/agda-calf/
Apache License 2.0
55 stars 2 forks source link

Implement merge sort #4

Closed HarrisonGrodin closed 3 years ago

HarrisonGrodin commented 3 years ago

Added decode to sum/unit, a la pi/sigma. (Is this okay, @kaonn?)

kaonn commented 3 years ago

Cool! A stylistic suggestion: you can factor out the module assumptions as a record in both insert sort and merge sort so they look more uniform.

HarrisonGrodin commented 3 years ago

Ooh, good call - done.