Online Otter-λ

Utility Link | Utility Link | Utility Link
ExternalSimplification | SetTheory | LambdaLogic | Induction | More >
-->

Examplessmall logo



Examples -> LambdaLogic -> lambda4.html


This file simply verifies the standard fixed point construction of lambda calculus. If you are not familiar with this construction, it is explained in Lambda Calculus. There is a also a discussion of this example in Implicit and Explicit Typing in Lambda Logic.