Structurally recursive nubBy

no obvious defects vs. obviously no defects

Structurally recursive functions obviously terminate. Convincing the termination checker about the original definition is quite simple, although not trivial.

https://gist.github.com/phadej/8ba28bc7ab955a4313d6.js
https://gist.github.com/phadej/fee248c9b6236790c30e.js

deleteFirst x (nub xs) ≡ nub (delete x xs)

The equivalence above is quite obvious, but wasn’t that easy to prove. Yet below is the mechanised proof.

--

--

Oh hai! How duz I program? Dunno. Kthxbye!

Love podcasts or audiobooks? Learn on the go with our new app.

Get the Medium app

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store
Oleg Grenrus

Oleg Grenrus

Oh hai! How duz I program? Dunno. Kthxbye!