Sergey Sinchuk

``` java.lang.NullPointerException at org.arend.typechecking.visitor.CheckTypeVisitor.addImplicitLamParams(CheckTypeVisitor.java:1503) at org.arend.typechecking.visitor.CheckTypeVisitor.typecheckImplementation(CheckTypeVisitor.java:1485) at org.arend.typechecking.visitor.CheckTypeVisitor.typecheckClassExt(CheckTypeVisitor.java:1356) at org.arend.typechecking.visitor.CheckTypeVisitor.visitNew(CheckTypeVisitor.java:1616) at org.arend.typechecking.visitor.CheckTypeVisitor.visitNew(CheckTypeVisitor.java:87) at org.arend.term.concrete.Concrete$NewExpression.accept(Concrete.java:829) at org.arend.typechecking.visitor.CheckTypeVisitor.checkExpr(CheckTypeVisitor.java:911) at org.arend.typechecking.implicitargs.StdImplicitArgsInference.infer(StdImplicitArgsInference.java:544) at org.arend.typechecking.visitor.CheckTypeVisitor.visitApp(CheckTypeVisitor.java:3100) at org.arend.typechecking.visitor.CheckTypeVisitor.visitApp(CheckTypeVisitor.java:3045) at org.arend.typechecking.visitor.CheckTypeVisitor.visitApp(CheckTypeVisitor.java:87) at org.arend.term.concrete.Concrete$AppExpression.accept(Concrete.java:402) at org.arend.typechecking.visitor.CheckTypeVisitor.checkExpr(CheckTypeVisitor.java:911) at org.arend.typechecking.visitor.DefinitionTypechecker.typecheckFunctionBody(DefinitionTypechecker.java:1285)...

Make LineMarkersPass constructor public

6

This would simplify life for plugin-writers and would allow them not to use workarounds.

Current implementation of class inheritance behaves poorly when parent class has external parameters. For example, it forces the user to write all inherited parameters of the parent class in a...

``` \func f {X : \Type} => X \where { \data D1 (n : Nat) \with | 0 => nilD X -- 'X' is not a reference to either a...

Reproducer with `func`: ``` \func f {X : \Type} => X \where { \class C { \func foo (_ : X = X) : X = X => idp \func...

Invoking :lib command does not add any new modules to the list of loaded modules. They seem to not appear in current scope either. The only thing that I've noticed...

Improve console REPL completion

2

Improve REPL completion. Currently `ImportCompleter` will not work on this example: ```\import Combinatorics.{-caret-}``` Instead default completion will add Fin (instead of BinOp and Factorial). Also make console completions smarter...

As stated. Should work similarly to :{ in ghci

In IDE PrettyPrintOptions button is greyed out for the following error: ```ERROR] Test.ard:19:27: Actual universe \Type is not compatible with specified universe \Type In: \Type```

Ctrl+P and ChangeSignatureRefactoring ignore implicit parameters.

1

Consider the following code block: ``` \func foo (x : Nat) => x \where \func bar => x ``` According to new Arend rules, function `bar` does have argument `x`...