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

(

*a*∧*b*) → (*b*∧*a*)

\z -> (snd z, fst z) :: (a, b) -> (b, a)

(

*a*→*b*→ c) → (*b*∧*a*) →*c*

\f -> \p -> f (snd p) (fst p) :: (a -> b -> c) -> (b, a) -> c

((

*a*→ (*a*→*b*)) ∧*a*) →*b*

\z -> let f = fst z x = snd z in f x x :: (a -> a -> b, a) -> b

\z -> fst z (snd z) (snd z) :: (a -> a -> b, a) -> b

To obtain proofs, convert the programs to proofs!

Destruction of a pair with

`fst`or`snd`means to apply ∧EConstruction of a function value means to apply →I

Etc.

Next | Next |