Yarrow is distributed with a number of example sessions, given below. We advise to read first how to try these examples in the most convenient way.
The example sessions are:
sessions/tutorialcontains a small tutorial session. The tutorial itself is available as
doc/sessions/tutor.ps. It is intended for people who are familiar with Pure Type Systems, but not necessarily with proof-assistants.
sessions/cubecontains the definitions of all systems of the lambda cube.
sessions/Uminuscontains the definition of the PTS lambda-U-minus, and shows its inconsistency.
sessions/logicdefines a PTS corresponding with a logic for reasoning about programs, and defines the usual logical connectives and the equality.
sessions/datatypcontains the definitions of the datatype
nat, using the impredicative encoding. (Yarrow has no inductive datatypes).
sessions/demoscontains demonstrations of the infix notation and the rewrite tactic.
sessions/thesiscontains the formal theory developed in my thesis.
Back to Yarrow Home Page