Equational Programming

Table of Contents

Pair

we try to find a method to combine two terms in a pair, in such a way that a component can be extracted from the pair.

definition of pair: π := λlrz.z l r

then: π P Q =β λz.z P Q

projection: