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
context of pattern variables on the left-hand side. Moreover, in
general, an eliminator can potentially refine that entire context. For
the datatypes we support, a case construct with a single scrutinee
doesn't really make sense, so we don't have one. The 'software'
approach, showing the impact of eliminators in a pattern matching style,
is more flexible anyway.
In the next version, we'll have local <=
f blah => g (lam stuff <= e {
lam stuff1 ...
...
lam stuffn ... })
but e will only be allowed to refine stuff, rather than the pattern
variables in blah.
I'd also like to have
f blah => g h where
h stuff <= e
h stuff1 ...
...
h stuffn ...
Especially when programming recursively, it's really important to keep a
grip on which bits of the context are considered parametric to an
elimination, and which should be quantified inside the motive. For plus
it doesn't matter, but for Ackermann it certainly does.
Cheers
Conor
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.
