generated at
チャーチペア
from Church encoding

チャーチブール値を用いると、2つの値の組を項として表現できる
型注釈はSystem Fによるもの


(m, n) = λb.b m n
b にチャーチブール値を入れることで m または n が得られる
数値型のタプルの場合 (m, n): PairNat
型注釈
数値型のタプルの場合
PairNat = ∀X. (CNat -> CNat -> X) -> X



fst = λx.x tru
fst (m, n) = m
数値型のタプルの場合
fst: PairNat -> CNat
snd = λx.x fls
snd (m, n) = n
数値型のタプルの場合
snd: PairNat -> CNat