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

“∨” means “or”

“

*a*∨*b*” means you have a proof of*a*, or you have a proof of*b*In logic if you can prove

*a*then you may conclude

*a*∨*b*you may also conclude

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

continued...

Next
Copyright © 2014 M. J. Dominus