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/
------------------------------------------------------------------------------
let (-----------!
! False : * )
False => all P : * => P
------------------------------------------------------------------------------
let (----------!
! True : * )
True => all P : * => P -> P
------------------------------------------------------------------------------
let (-----------!
! tt : True )
tt => lam P => lam p => p
------------------------------------------------------------------------------
( X : * !
let !-----------!
! not X : * )
not X => X -> False
------------------------------------------------------------------------------
( n : Nat !
data (---------! where (------------! ; !-------------!
! Nat : * ) ! zero : Nat ) ! suc n : Nat )
------------------------------------------------------------------------------
( n : Nat ; p : zero = suc n !
let !-----------------------------!
! znosuc n p : False )
znosuc n p <= case p
------------------------------------------------------------------------------
( n : Nat !
let !----------------------------------!
! zeronosuc n : not (zero = suc n) )
zeronosuc n => lam p => [<= case p]
------------------------------------------------------------------------------
