|Next||Types Are Theorems; Programs Are Proofs||14|
The proof rules match the rules for constructing functions!
Suppose you have a proof of some proposition
The last step is either →I or →E
Say it's →E.
Then we are concluding a from both a → b and a
So we have proofs of a → b and a
So we have programs of types a -> b and a
(Say f :: a -> b and x :: a)
Then f x :: b