agda/agda-stdlib — pull request #17 by pepijnkokke (2014-06-04 12:09:58+00:00)
Title: Adding `DecStrictPartialOrder` to Relation.Binary

Most orderings in Relation.Binary have a decidable variation. Three notable exceptions are Preorder, StrictPartialOrder and StrictTotalOrder (though the last of these is decidable in itself, by virtue of the `compare` function).

My commit adds implementations of DecStrictPartialOrder and IsDecStrictPartialOrder, and was tested against the HEAD version of Agda.