> Conor McBride wrote:
> Hi folks
>
> Knocked this up last week. Thought it might amuse...
I had always wondered why
( n : Nat ; P : Nat -> * !
let !-------------------------!
! Memo n P : * )
Memo n P <= elimNat n
{ Memo zero P => One
Memo (suc k) P => Pair (Memo k P) (P k)
}
doesn't build a slot for P zero's unless n is some (suc k). Didn't take
it serious enough, that in type theory everything starts with an E (for
elimination) and it requires you to bring your own proof for the base
case.
Best Regards,
Sebastian
