next up previous contents
Next: Definitions Up: The LEGO library - Previous: Quotient Types

Relations

There are two files, relations.l, and relclosure.l, which give elementary and infinitary lemmas about the algebra of relations. They pre-date the addition of primitive inductive types to LEGO, so use impredicative encodings to get "System F"-like inductive definitions.

In both files, a glaring omission is the failure to show that all the operations on relations introduced are in fact extensional with respect to EQRel. Much more could fruitfully be added.



 

Conor McBride
11/13/1998