John, can you help me with Cartesian powers? Following this example in the tutorial
let monotonic = new_definition `monotonic c <=> !q q'. q SUBSET q' ==> (c q) SUBSET (c q')`;; (* I tried this, and it works: *) let plane = new_definition `plane S Between Equiv <=> (Between SUBSET S /\ Equiv SUBSET S)`;; (* 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: *) let planex = new_definition `planex S Between Equiv <=> (Between SUBSET S^3 /\ Equiv SUBSET S^4)`;; (* Warning: inventing type variables Exception: Failure "new_definition: term not closed". *) let planexa = new_definition `planexa S Between Equiv <=> (Between:S->S->S->bool /\ Equiv:S->S->S>S->bool)`;; (* Same error message. *) -- Best, Bill ------------------------------------------------------------------------------ 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
