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.