theory Lambda imports Main begin term "\ f x. f (n f x)" (* abbréviation de type *) type_synonym 'a N = "('a \ 'a) \ ('a \ 'a)" definition zero :: "'a N" where "zero = (\ f x. x)" definition un :: "'a N" where "un = (\ f x. f x)" definition deux :: "'a N" where "deux = (\ f x. f (f x))" definition s :: "'a N \ 'a N" where "s n = (\ f x. f (n f x))" value "s deux" end