Next: and-elim digression | Prev: finite set family | Up: contents


After the style of the nat slide, this one also showed the hypotheses of the elimination rule appearing as the ghosts of the introduction rules by means of sliding the values down and across so that each i : fin n becomes Phi n i.

As you can perhaps work out, I slid the indices down, then the constructor patterns to the right. Rod thinks I should have slid the constructors down, then the indices to the left. He's right, you know.


Next: and-elim digression | Prev: finite set family | Up: contents


Conor's Work Page