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.
Conor McBride
11/13/1998