Julian / Julian/lean.nvim

Enhanced hover duplicates function arguments

Open
#519 0 comments 0 reactions 0 assignees View on GitHub
Dominant language
Lua
Stars
581
Forks
60
Avg merge
4d 12h
Merged PRs (30d)
2

Description

The enhanced hover handler prints a symbol's parameter list and then also prints the full type of the symbol after the colon. Parameters displayed before the colon are also represented in the function type after the colon.

For example, the hover for the `List` type shows:

```lean
List.{u} (α : Type u) : Type u → Type u
```

This seems to say that `List : Type → Type → Type`.

The notation as shown in the infoview and elsewhere is instead:

```lean
List.{u} (α : Type u) : Type u
```

Contributor guide

Open the contributing guide

Assessment

This issue has not been assessed yet.

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.