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*In logic if you can prove

*b*then you may conclude

*a*∨*b*(These are called ∨I)

(We will do ∨E shortly)

Next | Next |