None = λnone λsome (none)
Some = λval λnone λsome (some val)
Nil = λnil λcons (nil)
Cons = λh λt λnil λcons (cons h t)
// Scott Nats
S0 = λsλz z
S1 = λsλz (s λsλz z)
S2 = λsλz (s λsλz (s λsλz z))
S3 = λsλz (s λsλz (s λsλz (s λsλz z)))
S4 = λsλz (s λsλz (s λsλz (s λsλz (s λsλz z))))
S5 = λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz z)))))
S6 = λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz z))))))
S7 = λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz z)))))))
S8 = λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz z))))))))
S9 = λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz z)))))))))
S10 = λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz z))))))))))
S11 = λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz z)))))))))))
S12 = λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz z))))))))))))
S13 = λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz z)))))))))))))
S14 = λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz z))))))))))))))
S15 = λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz z)))))))))))))))
S16 = λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz z))))))))))))))))
S17 = λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz z)))))))))))))))))
S18 = λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz z))))))))))))))))))
S19 = λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz z)))))))))))))))))))
S20 = λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz z))))))))))))))))))))
S21 = λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz z)))))))))))))))))))))
S22 = λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz z))))))))))))))))))))))
S23 = λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz z)))))))))))))))))))))))
S24 = λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz z))))))))))))))))))))))))
S25 = λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz z)))))))))))))))))))))))))
S26 = λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz z))))))))))))))))))))))))))
S27 = λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz z)))))))))))))))))))))))))))
S28 = λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz z))))))))))))))))))))))))))))
S29 = λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz z)))))))))))))))))))))))))))))
S30 = λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz z))))))))))))))))))))))))))))))
S31 = λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz z)))))))))))))))))))))))))))))))
S32 = λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz (s λsλz z))))))))))))))))))))))))))))))))
Got = λlist (list GotN GotC)
GotN = λindex (None, Nil)
GotC = λh λt λindex ((index GotS GotZ) h t)
GotS = λi λh λt
let (got, t) = (Got t i)
(got, (Cons h t))
GotZ = λh λt ((Some h), (Cons h t))
Put = λlist (list PutN PutC)
PutN = λindex (index PutNS PutNZ)
PutNS = λi λval
let (old, t) = (PutN i val)
(old, (Cons None t))
PutNZ = λval (None, (Cons val Nil))
PutC = λh λt λindex ((index PutCS PutCZ) h t)
PutCS = λi λh λt λval
let (old, t) = (Put t i val)
(old, (Cons h t))
PutCZ = λh λt λval ((Some h), (Cons val t))
GenGotIndex = λindex λlist(Got list index)
GenPutIndexValue = λindexλvalue λlist(Put list index value)
main =
let list =
(Cons (Some S0)
(Cons (Some S1)
(Cons (Some S2)
(Cons (Some S3)
(Cons (Some S4)
(Cons (Some S5)
(Cons (Some S6)
(Cons (Some S7)
(Cons (Some S8)
(Cons (Some S9)
(Cons (Some S10)
(Cons (Some S11)
(Cons (Some S12)
(Cons (Some S13)
(Cons (Some S14)
(Cons (Some S15)
(Cons (Some S16)
(Cons (Some S17)
(Cons (Some S18)
(Cons (Some S19)
(Cons (Some S20)
(Cons (Some S21)
(Cons (Some S22)
(Cons (Some S23)
(Cons (Some S24)
(Cons (Some S25)
(Cons (Some S26)
(Cons (Some S27)
(Cons (Some S28)
(Cons (Some S29)
(Cons (Some S30)
(Cons (Some S31)
Nil
)))))
)))))
)))))
)))))
)))))
)))))
))
λfun
let (element, list) = (fun list)
element