Hi Bill,
| (* But that's not what I want. I thought the reference manual said that
| ^ means Cartesian power, so I tried something that didn't work: *)
It's true that ^ means Cartesian power, but on *types* rather than
*terms*. If you are happy to just use the universe of an arbitrary
type "S" as your basic set, then you could use the ^ constructor to
produce types of triples "S^3" or whatever. On the one hand, this
would be a bit easier because then the fact that p is a point is
implicit in the typing `p:S` and doesn't require a membership
assertion. On the other hand it is a bit less general that letting S
be an arbitrary subset of an arbitrary type.
There is no Cartesian power on sets predefined, though it would not
be hard to define it, and perhaps this is the right way to go.
Alternatively, you can use either of the following in place of S^3,
though they are a bit verbose:
`{(x,y,z) | x IN S /\ y IN S /\ z IN S}`
`S CROSS S CROSS S`
John.
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
