Let people explore programming in Agda without theoretical background.

Assumptions

- Most IT people are not interested in theory in the first place.
- One can go a long way without any theoretical knowledge in Agda.
- Theoretical remarks interrupt the programming experience.
- Students react quite differently to theoretical remarks.

(confused ↔ want to know a lot more)

- Students react quite differently to theoretical remarks.
- People who have already played with Agda are more open to theoretical background.

**Subgoals**- - give the syntax and semantics of Agda by examples
- - teach Agda programming skills
**Requirements**- - only secondary school mathematics is required
- - Haskell, type theory, and category theory knowledge is
**not**required **Audience**- - for newcomers
- - followable even without a tutor

Programmers should know equivalent solutions to be able to make design decisions.

*Hence we teach program transformations steps.*Programmers should know which solution is better to be able to make design decisions.

*Hence we add remarks to each program transformation step.*We teach how to do incremental program construction (planned).

- Teach data types first, functions later

There is a git repository located at GitHub:

https://github.com/mcmtroffaes/AgdaTutorial

You are welcome to submit pull requests (but please make small changes first)!

- Remain freely available and ready to fork
- Give citation of sources if applicable
- Try to merge with similar tutorials if any

This is the 6th semester we teach Agda at Eötvös Loránd University (ELTE) with the help of this tutorial.

- 13 weeks × 90 mins.
- Lecturer: Gábor Páli
- Past lecturers: Péter Diviánszky, Ambrus Kaposi
- We also learn a lot by teaching Agda :-)

import About.AIM_XVI -- The original slides for AIM XVI.