Tesla Zhang‮

Compiled file: https://github.com/JetBrains/intellij-community/blob/master/platform/core-api/src/com/intellij/psi/PsiCompiledFile.java

I wanted to do this....

Ironically, this will save us lots of time and cleans up many confusing code in intellij-arend if we adapted this approach from the beginning...

Is it created now?

Ok

According to @sxhya, the "import when selecting completion item" feature relies on the stub index, but they do work. Does that mean stub indices are created now?

Currently you can select an Arend expression and do Ctrl Shift P to show its type

FWIW the 'show type' action is kinda expensive

This is because how expressions are parsed. They are `BinOpSequence` in the Psi syntax. You can select expressions by abusing the 'show type' action -- put your caret on `==

Btw, are you a new Arend developer? You seem to be too active as a user :thinking: