§ Logical Predicates (OPLSS '12)
- has three conditions:
- (1) has type
- (2) has the property of interest ( strongly normalizes / has normal form)
- (3) The set is closed under eliminators!
- My intuition for (3) is that expressions are "freely built" under constructors. On the other hand, it is eliminators that perform computation, so we need to be closed under "computation" or "elimination"