Here are the slides of my TYPES 2015 talk “The troublesome reflection rule” with fairly detailed presenter notes. The meeting is taking place in Tallinn, Estonia – a very cool country in many senses (it’s not quite spring yet even though we’re in the second half of May, and it’s the country that gave us Skype).
Download slides: The troublesome reflection rule (TYPES 2015) [PDF].
Nice! A few comments/questions:
1. Some of the notes on the RHS of the slides are cut off at the end.
2. Doesn’t the eta-rule together with the reflection rule give you function extensionality?
3. Are you saying that the reflection rule is never applied (and, thus, an Eq-term in the context is never used) unless a hint explicitly instructs us to?
1. Fixed.
2. Yes, see examples/funext.m31
3. Yes, you get to choose which set of computation rules to use in each situation. (Of course, we plan to add flexible ways for manipulation of these.)