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/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.
sessions/cube contains the definitions of
all systems of the lambda cube.
sessions/Uminus contains the definition of
the PTS lambda-U-minus, and shows its inconsistency.
sessions/logic defines a PTS corresponding
with a logic for reasoning about programs, and defines the usual
logical connectives and the equality.
sessions/datatyp contains the definitions of
the datatype bool, list and nat,
using the impredicative encoding. (Yarrow has no inductive datatypes).
sessions/demos contains demonstrations of
the infix notation and the rewrite tactic.
sessions/thesis
contains the formal theory developed in my thesis.