idris2-tutorial

idris2-tutorial copied to clipboard

stefan-hoeck

[ wip ] chinese transition

1

use po4a extra po file. tranlate working on self-host weblate.

running-grass

If I didn't overlook it, it looks like the text doesn't contain the definition of `Prod` that appears in question 10 of Exercises part 2. > 10. Show, that the...

gemmaro

stefan-hoeck

Missing syntax

2

This is a non-comprehensive list of syntactic utilities I haven't yet explained in the tutorials. I'll update this whenever something else comes to mind. - [ ] Tuple sections -...

stefan-hoeck

[ doc ] Explain function application in the presence of infix operators

1

stefan-hoeck

Interface Exercises: Explain showPrec better or drop related exercises.

1

stefan-hoeck

Recently, using the name `empty` has led to strange disambiguation bugs, probably due to a conflict with `empty` from `Alternative`.

stefan-hoeck

[ new ] Chapter on details of QTT

3

A while ago (about a month ago at this point, oops) I offered to contribute a section in this tutorial explaining Quantitative Type Theory in depth. I've finally gotten around...

kiana-S

chuwy