Hi Note: Total = total ignoring non-termination, for this post
Surely we can assume them total given that base is never zero?
They are not total, they are called in a manner which does not cause them to raise an error. If you want every function to be total, you need to fix div. If you are happy with individual functions being partial, provided the program as a whole is total, that's fine (and I'd agree with you!). However, in this case you need to either prove that the program won't crash, or stop calling it total. This corresponds to proving that base is never zero. Of course, if you're going to just accept a proof that base is never zero, why not just accept a proof that head/tail are called on an infinite list? It says you defining codata, and your own versions of head/tail/drop etc I have a machine checkable (and machine generated) proof that base is never zero, and the list is infinite. Thanks Neil