Thorsten Altenkirch wrote:
Can you complete that proof?
Yes,
( n : Nat !
let !--!
! zeronosuc n : not (zero = suc n) )
zeronosuc n => znosuc n
That's not entirely facetious. You can only do 'pattern matching' on the
can you tell me why the second attempt to prove that zero is not a succ
fails?
There are several levels of explanation. First of all, if you have a look at the
syntax, e.g. section 3 of
http://www.dur.ac.uk/CARG/epigram/epigram-system.pdf
(no idea why this is still in Durham), you find that t
Hi,
can you tell me why the second attempt to prove that zero is not a
succ fails?
Can you complete that proof?
Cheers,
Venanzio
--
Venanzio Capretta
Department of Mathematics
and Statistics
University of Ottawa, Canada
http://www.science.uottawa.ca/~vcapr396/
---
