[Agda-dev] A tutorial on inference in Agda

[Roman]

Hi folks,

I wrote a painfully long tutorial on the way Agda does unification:
https://htmlpreview.github.io/?https://github.com/effectfully/unification-in-agda/blob/master/UnificationInAgda.html

It targets the users of Agda, so it doesn't cover advanced topics like
higher-order unification.

I'd like to hear your opinion before I share the link with a general
audience. Is there something horribly wrong there? What can be
improved? Are there any missing parts of the unification engine that
would be nice to cover? Is the tutorial readable in general? Any kind
of feedback would be highly appreciated.

Please don't share the link publicly yet.

BTW, I generate such HTMLs in an absolutely awful way. Does Agda
support generating an HTML page (with all the coloring) from an Agda
file when that file contains warnings, unresolved metas etc? And is
there a flag to make Agda accept ill-typed code, show a warning and
proceed with type checking? And color ill-typed code in red or
something, like unresolved metas are colored in yellow.

Best regards.