Ctrl+P and ChangeSignatureRefactoring ignore implicit parameters.

JetBrains / intellij-arend

Arend plugin for IntelliJ IDEA

Apache License 2.0

90 stars 12 forks source link

Ctrl+P and ChangeSignatureRefactoring ignore implicit parameters. #425

Closed sxhya closed 6 months ago

sxhya commented 1 year ago

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 when invoked from outside of where-block of foo. However, some Arend subsystem seem to have no support of this language feature:

[X] Ctrl+P feature
[X] ChangeSignatureRefactoring feature
[x] MoveStaticMembers feature

The exact arguments of bar can be calculated using the function Definition.getParametersOriginalDefinitions

sxhya commented 8 months ago

Partially addressed in a2820454eda43aebda4ec678640045b1a9fd45c2

sxhya commented 6 months ago

Fixed in 6f5c1290d2cfdeb22a5e7eac87c5cafb3e8eb498