I hope you don't mind me presenting inductive definitions in natural deduction style. Sorry folks, when you've got exciting dependent datatypes, you just can't get away with
Live, I construct the hypotheses of the elimination rule (induction) by stealing the structure of the introduction rules (counting), sliding the constructor patterns down so that each n : nat becomes Phi n.
Note that the horizontal dotted line is means the same thing as the conventional but annoying vertical line in natural deduction. The thing above the dotted line is a `hypothetical hypothesis'. Rod and I cooked up this notation one day, when he got fed up with me writing scary types on his blackboard.
Oh yeah, and here's the computational behaviour associated with natElim. It's like primitive recursion, but dependently typed and higher order.
Next: finite set family | Prev: opening credits | Up: contents