Konstantin Nisht

NPE in Arend serialization

3

``` Content=java.lang.NullPointerException at org.arend.module.serialization.ExpressionSerialization.writeBindingRef(ExpressionSerialization.java:63) at org.arend.module.serialization.ExpressionSerialization.visitReference(ExpressionSerialization.java:351) at org.arend.module.serialization.ExpressionSerialization.visitReference(ExpressionSerialization.java:31) at org.arend.core.expr.ReferenceExpression.accept(ReferenceExpression.java:34) at org.arend.module.serialization.ExpressionSerialization.visitApp(ExpressionSerialization.java:269) at org.arend.module.serialization.ExpressionSerialization.visitApp(ExpressionSerialization.java:31) at org.arend.core.expr.AppExpression.accept(AppExpression.java:72) at org.arend.module.serialization.ExpressionSerialization.visitApp(ExpressionSerialization.java:268) at org.arend.module.serialization.ExpressionSerialization.visitApp(ExpressionSerialization.java:31) at org.arend.core.expr.AppExpression.accept(AppExpression.java:72) at org.arend.module.serialization.ExpressionSerialization.writeExpr(ExpressionSerialization.java:161) at org.arend.module.serialization.ExpressionSerialization.writeType(ExpressionSerialization.java:51) at org.arend.module.serialization.ExpressionSerialization.writeParameter(ExpressionSerialization.java:134) at org.arend.module.serialization.ExpressionSerialization.writePattern(ExpressionSerialization.java:168)...

Don't use generated PSI in plugin

3

Arend's PSI tree is in fact a CST, not an AST. It results in a lot off difficulties with this tree: there are some strange nodes like `ArendAtomFieldAcc`, and the...

``` \func foo : Nat -> Nat => {?} \func bar => foo(1) ``` Yes, I know, it's a dumb case. Still the space should be inserted.

Sometimes it makes sense to replace a function passed as an argument with a lambda expression. It may arise when some implicit argument should be explicitly specified. Also, eta-long expressions...

``` \func a : 1 = 1 => idp \levels _ (0) ```

Intentions are not working properly for goals with arguments

1

At least, "Replace with constructors" is among them. 

Sized types allow defining inconsistent data

1

Consider the following data type: ```agda {-# OPTIONS --sized-types #-} module _ where open import Agda.Builtin.Size data ⊥ : Set where record SPN (i j : Size) : Set data...

Add type-based termination checker

15

This is a technical description of the pull request. For intro-level overview of type-based termination, consider reading [user manual](https://agda--7152.org.readthedocs.build/en/7152/language/type-based-termination-checking.html#). For deep semantical discussion of the process, consider reading [a paper](https://knisht.github.io/agda/msc.pdf)....

Preserve let-bindings when pretty-printing

2

Consider the following snippet. ```agda data U : Set where u : U test : U test = let X = U a : X a = u in {!helper...