[Agda] Decidable partial orders

Peter Berry pwberry at gmail.com
Thu Feb 25 18:19:54 CET 2010


I noticed the standard library has decidable total orders, but not
decidable partial orders. Implementing them was pretty straightforward
:) See the attachment. Disclaimer: I haven't tested it in any way.

I hereby release this code under the library's license.

-- 
Peter Berry <pwberry at gmail.com>
Please avoid sending me Word or PowerPoint attachments.
See http://www.gnu.org/philosophy/no-word-attachments.html
-------------- next part --------------
A non-text attachment was scrubbed...
Name: DecPartialOrder.agda
Type: application/octet-stream
Size: 1071 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20100225/7db75bf1/DecPartialOrder.obj


More information about the Agda mailing list