Seems the implementation is Haskell, would've been much cleaner in Ocaml. Appearently it's a grad coruse in functional algorithms but can't even see the time-complexity analysis of heapify.
> The programs in this book are written in Isabelle’s functional programming language
From what I can tell, Binomial Heaps also have a runtime analysis. Not sure what you’re referring to with “heapify.”
I would encourage others to ignore this snide comment. I have read other books from the authors, particularly Concrete Semantics, and it’s honestly incredible what can be achieved with Isabelle. Obviously it’s not going to be interesting if formal verification isn’t your thing, but if it is, the content is priceless.
