Alex Gryzlov

I've rolled back to 0.3.1, haven't updated it since.

No, nothing critical, I was just curious about porting old examples, e.g. https://github.com/tixxit/optimistic-spec-article I guess, let's wait for Dotty then :)

Ah, we're just missing `%default total` in the header of the file, thanks.

Probably not without some kind of preprocessing.

Ok, my current take is simply to write out all the induction principles by hand there. Then we should find some Idris expert to edit the text and describe how...

Hey, thanks for the help! I'll try to review in the next few days.

I see you have added the `Types` chapter, so I changed the name on this PR :)

So, just to let you know, I've started reviewing `Smallstep` at last, got almost halfway through it.

@jutaro I've pushed my WIP post-review fixes for `Smallstep` directly on this PR, hope you don't mind?

Oops, pushed an update.