Inference in Agda

This is a tutorial on how Agda infers things.

How to read

There are two ways to read the tutorial:

1. click this link to read the rendered HTML. Simple and sufficient, if you only want to read and not play with the code or contribute
2. if you do want to play with the code, then install Agda, clone the repo, open the InferenceInAgda.lagda.md file, type check it and only then read

IMPORTANT: reading InferenceInAgda.lagda.md without type checking the file beforehand is a non-option as making Agda color the code is important for understanding how things get type checked. Hence reading InferenceInAgda.lagda.md directly on GitHub is a non-option as well as GitHub's syntax highlighting is insufficient and the file has to actually be type checked.

Contributing

Building the HTML is a bit of a PITA as it requires several tools to be installed and several commands to be executed. So if you're going to create a PR, don't bother updating the HTML file, I'll do that myself.

Building the HTML

Prerequisites

1. install agda and its standard library
2. install htmlize for emacs. For example via (use-package htmlize :ensure t)
3. install agda-html-to-md
4. install pandoc
5. add this to your .emacs.d file:

(global-set-key (kbd "C-x a h") 'htmlize-buffer)
(fset 'generate-inference-in-agda-html
  [?\C-x ?h ?\C-u ?\M-| ?a ?g ?d ?a ?- ?h ?t ?m ?l ?- ?t ?o ?- ?m ?d return ?\C-x ?h ?\M-| ?p ?a ?n ?d ?o ?c ?  ?- ?- ?t ?o ?c ?  ?- ?s ?  ?- ?o ?  ?I ?n ?f ?e ?r ?e ?n ?c ?e ?I ?n ?A ?g ?d ?a ?. ?h ?t ?m ?l return])
(global-set-key (kbd "C-x a i") 'generate-inference-in-agda-html)

Generating the HTML

IMPORTANT: wait for each command to finish.

1. open InferenceInAgda.lagda.md in emacs
2. C-c C-l (type check the file)
3. C-x a h (initial htmlization of the buffer)
4. C-x a i (generate the final InferenceInAgda.html file)