- The directory
`sessions/tutorial`

contains 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. - The directory
`sessions/cube`

contains the definitions of all systems of the lambda cube. - The directory
`sessions/Uminus`

contains the definition of the PTS lambda-U-minus, and shows its inconsistency. - The directory
`sessions/logic`

defines a PTS corresponding with a logic for reasoning about programs, and defines the usual logical connectives and the equality. - The directory
`sessions/datatyp`

contains the definitions of the datatype`bool`

,`list`

and`nat`

, using the impredicative encoding. (Yarrow has no inductive datatypes). - The directory
`sessions/demos`

contains demonstrations of the infix notation and the rewrite tactic. - The directory
`sessions/thesis`

contains the formal theory developed in my thesis.

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: