Hi
-- There are no pattern-matching failures here.
-- The totality is harder to see: all digits are roughly of the same range,
-- but each recursive call increments base. Eventually, base becomes bigger
-- than d+9 and so the first alternative will be selected, which is in the
-- WHNF and so
On Tue, 13 Mar 2007 10:17:05 +
Neil Mitchell [EMAIL PROTECTED] wrote:
Hi
-- There are no pattern-matching failures here.
-- The totality is harder to see: all digits are roughly of the
same range, -- but each recursive call increments base. Eventually,
base becomes bigger -- than
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
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 Nicolas,
It seems like we could refine the first parameter of carryPropagate
just as the second: make an= type N1 that only admits values [1..].
How?
newtype N1 = N1 Int
(put that in a module and don't export N1)
define the constant 2, define the increment operator, change div and mod.
Neil Mitchell wrote:
newtype N1 = N1 Int
(put that in a module and don't export N1)
define the constant 2, define the increment operator, change div and mod.
That is precisely what I would have done.
Now we've mainly got a proof in the type checker, but we still don't
actually have a
