valis
valis
When a file is open in REPL, it would be convenient to import not only the file itself, but also all imports in the file.
Allow let definitions in REPL. E.g., ``` > \let x => 3 > x + x 6 ```
``` java.lang.IllegalStateException at org.arend.core.context.param.EmptyDependentLink.getType(EmptyDependentLink.java:73) at org.arend.core.context.param.DependentLink.getTypeExpr(DependentLink.java:47) at org.arend.typechecking.subexpr.CorrespondedSubExprVisitor.visitParameter(CorrespondedSubExprVisitor.java:316) at org.arend.typechecking.subexpr.CorrespondedSubExprVisitor.visitSigmaParameters(CorrespondedSubExprVisitor.java:341) at org.arend.typechecking.subexpr.CorrespondedSubDefVisitor.visitFunction(CorrespondedSubDefVisitor.java:74) at org.arend.typechecking.subexpr.CorrespondedSubDefVisitor.visitFunction(CorrespondedSubDefVisitor.java:21) at org.arend.term.concrete.Concrete$BaseFunctionDefinition.accept(Concrete.java:2128) at org.arend.refactoring.ArendSubExprUtilsKt.correspondedSubExpr(ArendSubExprUtils.kt:163) at org.arend.refactoring.ArendSubExprUtilsKt.tryCorrespondedSubExpr(ArendSubExprUtils.kt:175) at org.arend.intention.SplitAtomPatternIntention.getElementType(SplitAtomPatternIntention.kt:133) at org.arend.intention.SplitAtomPatternIntention.isApplicableTo(SplitAtomPatternIntention.kt:51) at org.arend.intention.SelfTargetingIntention.getTarget(SelfTargetingIntention.kt:62) at org.arend.intention.SelfTargetingIntention.isAvailable(SelfTargetingIntention.kt:78) at com.intellij.codeInsight.intention.impl.ShowIntentionActionsHandler.availableFor(ShowIntentionActionsHandler.java:157)...
Currently, the type of parameters and the result type of functions defined in instances can be inferred only when it does not mention other fields of the class. It should...
It should be possible to have external libraries without sources. Even if a library has sources, we do not need to load them. We also don't have to load them...
An unnamed variable (i.e., _) can be given a name in an error message. For example, consider the following code: ``` \func foo {A : \Type} (B : A ->...
If the expected type of `e` is a class and its actual type is the type of the classifying field of the class, then `e` can be replaced with the...
Suppose that `A` coerces to `B`. Then it's not true that `C -> A` coerces to `C -> B`. We can fix that. Similarly, we can make `a = {A}...
Currently, pi-types and sigma-types are not allowed in classifying expressions of instances. Also, only a restricted form of lambda expressions is allowed.
ST monad
We can implement an analogue of ST monad. It will be built-in in core and will allow more efficient implementation of various algorithms. They can be verified through the usual...