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.
Lego
1998-06-15