search

Julian / lean.nvim

neovim support for the Lean theorem prover
MIT License
255 stars 25 forks source link

Go-to-definition in Lean 4 widgets #258

Closed gebner closed 2 years ago

gebner commented 2 years ago

Depends on https://github.com/leanprover/lean4/pull/1157

Julian commented 2 years ago

The jumps seem weird though -- I see discussion still happening upstream a bit, but e.g. if I open some random mathlib4 file like Algebra/GroupWithZero/Defs.lean and sit on line 6 to try this out, my infoview state says:

▶ expected type (6:3-6:11)
M₀ : Type u
toMul : Mul M₀
mul : M₀ → M₀ → M₀ := Mul.mul
toZero : Zero M₀
zero : M₀ := Zero.zero
zero_mul : ∀ (a : M₀), 0 * a = 0
⊢ ∀ {M₀ : Type u} [self : MulZeroClass M₀] (a : M₀), 0 * a = 0

heading to toZero : Zero M₀, on Zero, gd and gt do nothing, gD takes me to the definition of function application in src/Lean/Parser/Term.lean.

gebner commented 2 years ago

heading to toZero : Zero M₀, on Zero, gd and gt do nothing

You should be able to gd on Zero.zero. Any function application, like Zero M₀, doesn't work yet.

Julian commented 2 years ago

Ah sorry, I misread that comment previously. Got it, thanks.