Tesla Zhang‮

Did you mean to open an issue in the Arend repo? 🤣

> Also, it might be a good idea to update the language version for the tutorial, so that users don't get distracted when they try it these days. Yes, this...

I agree with OP.

``` ab ==< b >== a ==< b >== ``` should be formatted to ``` ab ==< b >== a ==< b >== ```

It might be a separate formatter?

It's the pretty printer

Oh, sorry, I remembered it wrongly.

https://github.com/JetBrains/intellij-arend/blob/1c110f1081154aa297aeb8f3a0e8af0c48803965/src/main/kotlin/org/arend/quickfix/GoalFillingQuickFix.kt#L13

At least refactor nls strings with `ArendBundle.message` or something.

nokogiri :thinking: