Agda-2.3.2.2: src/prototyping/terms/example.lam

id = \x -> x;
k  = \x -> \y -> x;
s  = \x -> \y -> \z -> x z (y z);

foo;

foo' = id foo;

id' = s k k;

sk = s k;

-- zero; suc;
-- one = suc zero;