6 Handouts

\(\newcommand{\la}{\lambda} \newcommand{\Ga}{\Gamma} \newcommand{\ra}{\rightarrow} \newcommand{\Ra}{\Rightarrow} \newcommand{\La}{\Leftarrow} \newcommand{\tl}{\triangleleft} \newcommand{\ir}[3]{\displaystyle\frac{#2}{#3}~{\textstyle #1}}\)

Here are some pages with additional helpful information. These are linked at places in other chapters and collected here for convenience.

Quote notation and pattern matching.

The halting problem.

Agda tips and suggestions.

Interacting with asciicasts.

Proust code:

proust-imp-basic.rkt

proust-imp-with-holes.rkt

proust-pred-start.rkt

proust-just-comp.rkt

proust-pred-forall.rkt

proust-pred-eq.rkt

proust-pred-bool.rkt

proust-pred-forall-db.rkt

proust-pred-forall-db-holes-basic.rkt

proust-pred-forall-db-holes-tactics.rkt

proust-pred-forall-db-holes-unif.rkt

Starter Agda files (starting point for exposition in the text):

nothing.agda

logic.agda

ordering.agda

equality.agda

nat.agda

sorting.agda

braun.agda

Completed Agda files (holes are for exercises):

nothing.agda

logic.agda

ordering.agda

equality.agda

nat.agda

sorting.agda

braun.agda

Coq files:

bool.v

logic.v

nat.v

sort.v