| 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 ∧E
Construction of a function value means to apply →I
Etc.
| Next | Next |