I'm working on a mizar article in which I have defined an operation
`sum' on terms of type a := `Subset of {0,1}' and an operation, say f, each
of whose values has the type `Element of {0,1}'. I'd like to have the
term
t := { f(x) : A(x) },
where A(x) is some formula, to have the type a, so that
sum({f(x) : A(x)})
is a well-formed term. Currently, the last expression is not
well-formed; I get error 103 ("Unknown functor") underneath the last
character `m' of `sum'. My guess (though of course I may be mistaken)
is that I get this error because t is not known, syntactically, to
have the type a. On this assumption, my question is: is there a
simple way of getting t to have type a? (I suppose that there's
another way to accomplish what I'm trying to do without requiring the
term in question to have the indicated type, but it seems to me that
somehow automatically assigning the term the type a is the most
natural way to solve the problem.) Is there some part of the MML or
mizar language that I'm missing here, or would the parser need to be
modified to accomplish what I'm describing?
Any recommendations would be appreciated!
Thanks,
Jesse
--
Jesse Alama (alama@stanford.edu)