[syrak]

> I do wonder why people keep building more systems of this kind.

Not a lot of languages have higher-inductive types which is the main advertised feature here. At least they're missing in Isabelle and Coq.

That's also orthogonal to the matter of automation/metaprogramming, which, from the lack of mention, doesn't seem to be their focus right now. There doesn't seem to be anything fundamentally in the way of Coq-style tactics either if they really wanted to build that on top of what is presented here.

[tom_mellior]

True, there are probably no theoretical obstacles. But there is a huge implementation effort, and judging from other new proof assistants that started out without tactics, I wouldn't hold my breath.

Unless you desperately need exactly this kind of fancy logic, if you actually want to get stuff done, you would choose a different system. That's not great if they are interested in wide adoption.