Installing Ubuntu (or other distribution) packages will usually give you old, but matching versions of the standard library.
You then may need to follow the section “Until Agda-2.4: Setting up the Emacs mode for use with the library” on the Agda standard library page.
Get started with the textbook Programming Language Foundations in Agda (PLFA).
Download the source:
git clone https://github.com/plfa/plfa.github.io.git
The files corresponding to the early sections of the book
are in the sub-directory src/plfa/part1
,
see the ``Source'' links at the top of the web pages corresponding
to each section.
Work through the first four sections and complete at least all “recommended” exercises: For each section, produce a copy of the source file and complete at least the indicated exercises:
_^_ (power)
and
∸-examples (monus-examples)
+-swap
,
times-distrib-plus
,
+-assoc
— try also at least
*-comm
,
0∸n≡0
, and
∸-+-assoc
<-trans
,
trichotomy
, and
≤-iff-<
Equality: After the repeated proof of commutativity (and the explanations for it), insert a proof for
+-assoc : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
that proceeds by induction on n
.
(If you get stuck, you may find some inspiration in the proof of
+-rearrange
in Induction
.)
You may remove explanations except for parts about which you insert questions into the document, and except the Exercise descriptions. You are encouraged to insert your own documentation, questions, descriptions of problems you encountered and how you solved them as literate documentation between the code fragments.
Do not remove Agda code!
(The PLFA source files are literate Agda files using MarkDown for
the documentation parts; this is one of the acceptable formats for
this course. After loading such a *.lagda.md
file in Emacs, you
may need to manually start M-x agda2-mode
to activate the special
Emacs mode for Agda, which will also give you an ``Agda'' menu in
the Emacs menubar.)
CAS763
for your submissions
(so that you can have other directories for other purposes),
and deposit your submission files for Assigment 1 in the
sub-directory CAS763/A1
.
Give me (kahl
) access to this repository and send me a link.