valis

After using the tracer the status of the definition is reset to untypecheked it seems.

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.

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

False negative "redundant parentheses" error

1

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

Redundant parentheses are not reported in the following code: ``` \func foo (F : Nat -> \Type) => (F 0) -> (F 0) ```

In the following code, parentheses are redundant: ``` \func bar {x : \Sigma Nat Nat} => x.1 \func foo => bar {(1,2)} ```

Import action may perform slow operations ``` java.lang.Throwable: Slow operations are prohibited on EDT. See SlowOperations.assertSlowOperationsAreAllowed javadoc. at com.intellij.openapi.diagnostic.Logger.error(Logger.java:182) at com.intellij.util.SlowOperations.assertSlowOperationsAreAllowed(SlowOperations.java:110) at com.intellij.util.indexing.FileBasedIndexImpl.ensureUpToDate(FileBasedIndexImpl.java:754) at com.intellij.psi.stubs.StubIndexImpl.getContainingIds(StubIndexImpl.java:501) at com.intellij.psi.stubs.StubIndexImpl.processElements(StubIndexImpl.java:305) at com.intellij.psi.stubs.StubIndex.getElements(StubIndex.java:100) at...

Implement various quick fixes: - [x] All errors with WARNING_UNUSED level -- remove some part of the expression - [x] ArgumentExplicitnessError -- make explicit/implicit - [x] InstanceInferenceError (without classifying fields)...

Pressing enter in the following code sends the expression to the beginning of the line. ``` \module M \where { \func foo (x : Nat) : Nat => {-caret-}\case x...

Navigation from source does not work for errors embedded in goals.