Josef Urban <urban@ktilinux.ms.mff.cuni.cz> writes:
On Wed, 22 Nov 2006, Jesse Alama wrote:
Josef Urban <urban@ktilinux.ms.mff.cuni.cz> writes:
I think the problem is that the type "0-chain of p" does not
syntactically widen to "Element of ..." . I checked just now, and it
seems that non-emptiness is no longer a problem. So yes, this really
has to be done syntactically in the (re)definition of "0-chain of"
like
mode 0-chain of p -> Element of foo means ....
If it is e.g. just a proved theorem, Mizar will take no notice.
I see now, thanks. If I choose to not redefine 0-chain of p, what
form should the theorem take?
just to repeat for sure: if you choose not to have the type widened
through (re) definitions into Element of ..., the fraenkel term will
not work (with the current implementation)
Oh, I see, I misunderstood: I thought that there were two approaches
to solving the problem (redefinition, prove a theorem), but now I see
that only one of these (redefinition) solves the problem.
I've written the redefinition as follows:
definition let p be polyhedron;
redefine mode 0-chain of p -> Element of Funcs(vertices(p),{0,1});
::> *118
end;
Error 118 is: "Invalid specification". The redefinition is broken but
the error I had with the fraenkel term goes away. I'm not sure what
the problem is with my redefinition. Curiously, I also get the same
error when I replace `Element of Funcs(vertices(p),{0,1})' with a much
wider type:
definition let p be polyhedron;
redefine mode 0-chain of p -> set;
::> *118
end;
What might be going on here?