> The big difference between Idris 1 and Idris 2 is that Idris 2 represents the context as an array, with constant time access and update. Yes, it's mutable! We recognise that there's going to be a lot of updates: mainly solving unification problems as type checking proceeds, but also during interface resolution. Ждём разоблачающий пост Зефирова с очередной рекламой HAMT и прочих иммутабельных структур.