[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: Phonebook example from WIFT'95 paper not working?


The tutorial isn't quite as precise as it could be here: you also need
the apply-extensionality command described in the preceding discussion
of the failed proof for "deladd" (and for the same reason--you're
trying to establish equality of two functions).

Thanks for bringing this to our attention; we'll improve the wording.
Note that you can often make progress when you're stuck by sneaking
a look at the proofs in the PVS dump file that goes with the WIFT
tutorial (and linked to it on the web site).