intellij-arend

intellij-arend copied to clipboard

Stubs do not work

5

It seems that stubs for PSI elements are never created.

valis

Equational reasoning style support in formatter

3

It would be nice if the formatter could recognize equational reasoning style. Alternatively, the user could provide hints in comments specifying "this block should be formatted as equational reasoning style."

tonyxty

Make a separate subsystem for resolving. Highlight and PsiReference.resolve should just invoke this subsystem.

valis

So repl can have highlighting.

ice1000

Save history in REPL

2

As title.

ice1000

Generate signatures for field implementations in instances

1

Signature of functions defined in instances (and other functions) must be specified explicitly. It is possible to generate them automatically. This can be implemented as an intention. Before: ``` \class...

valis

Invoke the doubleChecker in IDE plugin

1

Maybe it should be an option in the gutter icon of each definition?

ice1000

ice1000

Unused local variable/binding

1

If a local let binding is unused, we may ask the user to remove it. If a local binding is unused, we may ask the user to rename it to...

ice1000

When "Goto declaration or usages" (i.e., ctrl+click) is invoked on a declaration, it should show all of its usages, but this does not work in Arend.

valis