search

pufferffish / agda-symmetries

MIT License
5 stars 1 forks source link

Prove Bag is CMon #66

Closed pufferffish closed 8 months ago

pufferffish commented 8 months ago

Close #54

pufferffish commented 8 months ago

autToLehmer turned out to be very annoying to prove because of the sheer amount of noise that comes with inspect encode (isoToEquiv aut). Agda would basically run out of memory so an alternative approach is needed.