JetBrains / intellij-arend

Arend plugin for IntelliJ IDEA
Apache License 2.0
90 stars 12 forks source link

`Shift+Ctrl+P` should actually typecheck pieces of code upon which it is invoked #430

Closed sxhya closed 3 months ago

sxhya commented 1 year ago

Current implementation only allows you to see type information that has been dumped and stored during the typechecking process. Due to peculiarities of typechecking this process currently is not 100% reliable (e.g. there is no guarantee that the typechecker will actually infer types for all the subexpressions of a given expression). This also makes Shift+Ctrl+P feature reliant upon the correct operation of autoretypecheck feature.