intellij-arend

intellij-arend copied to clipboard

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...

knisht

```tex \func def \alias defalias (n : Nat) : Nat | 0 => 0 | suc n => defalias n \func usage => defalias ``` 1. Put the caret at...

marat-rkh

Improve UI around "Project SDK" field in the project wizard

3

 Project SDK is needed if you want to create a language extension or debug typechecking. It would be nice to add this information to the UI, say, it the...

marat-rkh

``` 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)...

sxhya

We can implement an intention that changes the explicitness of parameters. It can also produce warnings when an explicit arguments should be made implicit and vice versa.

valis

``` \func test (f : Nat -> Nat) : Nat => \case (f 0) \with { | 0 => 0 | suc n => n } ```

valis

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

knisht

False negative "redundant parentheses" error

1

The warning isn't shown in the following code: ``` \func test => \Sigma (Nat) (Nat) ```

valis

In Emacs mode for Coq, we can view the diff between expected and actual types in typechecking errors. This could be useful when types are large and it is not...

marat-rkh

Consider showing math symbols instead of some language constructions

1

In Emacs mode for Coq (with company-coq), there is a special mode that shows math symbols instead of some language constructions, like lambdas, `forall` quantifier, etc. With prettify-symbols-mode off: With...

marat-rkh