Raitis Veinbahs more about me my toy projects my github my asciinema

Proving binary string bijection with naturals in agda

June 5, 2022

Here’s (github.com/siers/agda-plfa) my solution to the exercise «Bin-predicates (stretch)» from the PLFA book’s «Relations» chapter which proves that the binary string ADT and the conversions defined as to and from do indeed form an bijection (isomorphism) with the naturals.