Is there any theory about partial orders in HOL4?
I have been party to some work on the partial order of lazy lists under the prefix relation (in particular proving that it is complete). It would be nice to instantiate (or create?) some general theory, although going too far in that direction probably pushes the limits of HOL.
------------------------------------------------------------------------------
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
