module LambdaCalculus where

{- λ-исчисление не требуется определять в языке Agda, поскольку Agda
   является его расширением.  Достаточно лишь не использовать определённые
   свойства языка Agda, а именно, зависимые типы, полиморфизм и индуктивные
   типы.  При этом нетипизированное исчисление это просто исчисление с
   единственным типом.

   Однако для λ-исчисления нельзя построить модель, то есть множество D,
   которое содержит _все_ функции на D.  Тем не менее, её можно построить,
   если ограничиться только некоторыми функциями (D.Scott).

-}

