15 lines
354 B
Plaintext
15 lines
354 B
Plaintext
-- id_0.lc
|
|
let id = \x -> x
|
|
let zero = \f x -> x
|
|
|
|
eval id_zero:
|
|
id zero
|
|
=d> (\x -> x) (\f x -> x) -- expand definitions
|
|
=a> (\z -> z) (\f x -> x) -- alpha rename
|
|
=b> (\f x -> x) -- beta reduce
|
|
=d> zero -- expand definitions
|
|
|
|
eval id_zero_tr:
|
|
id zero
|
|
=*> zero -- transitive reductions
|