[ProofPower] Type-check bug?

[Roger Bishop Jones]

Steve,

Its pretty hard to diagnose your problem without
even seeing the goal!

If you really want to report a bug you should
prepare a sanitised document which exhibits the
bug and which you are free to disclose.
Even if you want good advice that would be a
good idea.

Guessing rather wildly I would suspect that
the "f" you are trying to offer a witness for
is the first name in the signature of an 
existential which has more than one name in
its declaration part.

In that case, though in a similar HOL
existential you could offer a witness
just for the "f", in Z you can't do that.
You have to offer a witness for the entire
signature of the existential, as a binding.
Offering a single value as a witness not
as a binding, is a supported special
case, but can only be done if the signature
has only one name in it.

NB I think the ProofPower syntax for bindings is
different to the one in the standard.
I see that the Z tutorial is pretty bad in this
area, but if you look in the solutions to the
exercises for goal oriented predicate calculus
proofs you will see some examples.
usr011 section 8.1.4.

Roger Jones