How to try these Yarrow sessions

It is most convenient to use Yarrow in combination with a windows system. I suggest you have two windows to try these example sessions in Yarrow: For example, load the file sessions/example/exam.ys in the text editor and drag the first line to Yarrow. You will see
> prove silly : @P:*.P->P
@P:*. P->P

Dragging the next line to Yarrow will result in
$ intros then assumption
Goal proved!

And the last line will give
$ exit
prove silly : @P:*. P->P
intros then assumption

silly := .. : @P:*. P->P

Sometimes you will drag multiple lines to Yarrow which may result in the input and output not to be interleaved correctly. Blame your windows system for this.

When you start working on your own proofs in Yarrow, you typically work in the same way, with one window containing Yarrow and one containing a text editor with the session you are working on. Then the text is dragged in the other direction, from the Yarrow window to the editor window. This works easy because after the end of a proof, Yarrow gives a summary of all the commands that were used.

Back to the example sessions page
Back to Yarrow Home Page