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 the "by rule" ("<=") is
only applicable
in a program, i.e. on the top level. That is currently Epigram does not support
local
pattern matching - but this is a frequently requested feature (called the "with"
rule in "The view
from the left") and should be included in the next major release.
It is maybe good to notice that epigram programs are actually program tactics
which generate
type theoretic code. As a consequence you are not limited to use the gadgets
provided (case, rec)
but you may write your own eliminators and hence invent your own notion of
patterns. For
an example you may have a look at 6.1 of
http://www.cs.nott.ac.uk/~txa/publ/ydtm.pdf
Can you complete that proof?
Yes,
( n : Nat !
let !----------------------------------!
! zeronosuc n : not (zero = suc n) )
zeronosuc n => znosuc n
Cheers,
Thorsten
--
Dr. Thorsten Altenkirch phone : (+44) (0)115 84 66516
Lecturer http://www.cs.nott.ac.uk/~txa/
School of Computer Science & IT University of Nottingham
This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.
