-
Notifications
You must be signed in to change notification settings - Fork 0
Exotic Types
Jonathan Sterling edited this page Jun 30, 2014
·
1 revision
Some notes on adding further fancy Nuprl-style types.
These will be very straightforward. Squashed reflexive-transitive closure of an arbitrary relation.
The binary version of these isn't difficult: for a <= S∪T, either a <= S or a <= T. Likewise, for a <= S∩T, both a <= S and a <= T.
It is not immediately clear how to do these in our type theory without making things undecidable. Perhaps an extension to the reflect mechanism...
These will probably be easy. For a <= [x:S]∩T, we just have to check that a <= S and a <= [a/x]T.