Next | Types Are Theorems; Programs Are Proofs | 20 |

-- x :: a -- y :: b (x, y) :: (a, b)

In logic if you can prove

*a*and you can prove*b*,Then you may conclude

*a*∧*b*(This is called ∧I)

continued...

Next
Copyright © 2014 M. J. Dominus