Against all likelihood I remembered to post this! The sigma type syntax has changed from (x | P x) to (x ** P x), so that’s reflected. Other than that, though, the colours of proof tactics and builtin syntax have been changed. I think that’s all.

Pow!

I also stuck it on patch-tag, but since it wasn’t darcsed until about a minute ago, the history isn’t very exciting yet.

Edit: don’t use this; the tactic colouring is flaky and doesn’t work. I’ll revert it and post a new version in a bit.

Anyone use Idris? You should, it’s good.

Anyway, I made a Vim syntax for it. Beware the indent is rubbish, due to the old chestnut that context free languages are a bit tricky to recognise using regular expressions. Colouring things in is easier because most of it is just looking for certain tokens (which, of course, really is regular in most/all languages).

Anyway, this. I might even remember to upload updates when I do them¹, who knows.