It seems like we could refine the first parameter of carryPropagate just as the second: make an= type N1 that only admits values [1..]. Would not that suffice to prove that base is never 0 and not have to go beyond the type-checker for a proof?
On 3/13/07, Neil Mitchell <[EMAIL PROTECTED]> wrote:
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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe