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


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.