# The troublesome reflection rule (TYPES 2015 slides)

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).

Mike Shulman

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.)
Write your comment using Markdown. Use $⋯$ for inline and $$⋯$$ for display LaTeX formulas, and <pre>⋯</pre> for display code. Your E-mail address is only used to compute your Gravatar and is not stored anywhere. Comments are moderated through pull requests.