[isabelle] "partial order" type?
I want to write a function that takes a partial-order as a parameter. Specifically, I want the following function...
fun interleave :: "'a list => 'a list => 'a partialorder => 'a list set"
... which takes two lists and a partialorder, and returns the set of all interleavings of the elements of those lists which respect the partial order.
I know that I could replace "'a partialorder" above with "('a \<times> 'a) set", and then prove a lemma saying "if that parameter is a partial-order then interleave has such-and-such a property". But it would be rather nice just to put the partial-order-ness of that parameter straight into its type. Can I do that, and if so how?
Thanks very much,
This archive was generated by a fusion of
Pipermail (Mailman edition) and