top
|
next
The usual definition of lambda-terms
The set of lambda-terms, L, is defined inductively:
x is in L
M in L implies (\x.M) is in L
M, N in L implies (MN) is in L
where x is an arbitrary variable.