valis

Anyway, the problem is `pmap (transport id) idp`. Arguments for `pmap` cannot be inferred from `idp` (since they are not specified there, but they are specified in `lemma` so it...

You can add a flag to our run configuration.

No, they're not. I think this might be because of serialized core expressions. When they're loaded, it looks at PSI elements which might cause creating the whole element instead of...

Indices do work, but stubs are never created, instead actual PSI elements are always created (not their stubs).

A similar problem: ``` \func test => (Array Nat) -> (Array Nat) ```

Now, it extends a little bit, but then jumps to the whole expression anyway.

It's a bug in BasePass. At line 195 we pass `expr.textRange` to `replaceExprSmart`, but that's incorrect since we need to compute the actual deleted range. I think this functionality was...

Probably a duplicate of #299.

I thought it just syntactically inserts the expression. Why does it invoke pretty printer?

This is actually kind of the point. We allow a restricted range of Unicode symbols because otherwise there will be a large number of incomprehensible and almost identical ones. We...