Asking about VSCode Lean Features

Stream: new members

[Noah Stebbins]

Hey guys,

A few things I'm curious about with people that use VSCode to write Lean code.

1. For cases where there's a lot of inheritance of type classes, is there a way you guys easily can visualize the type hierarchy? In VSCode, there's > Types: Show Type Hierarchy but it doesn't seem to work with Lean structures. For example, if I type a keyboard shortcut while my cursor is over Group, I'd love to see a tree that has Group as the root and branches out to DivInvMonoid which branches out to Monoid, Inv, Div and so on...
2. I noticed that I can't lookup every reference in VSCode. To be precise I'm referring to editor.action.revealDefinition in VSCode. It would be really lovely to have this always work. For example, when I type out this code below, I can use my keyboard shortcut for editor.action.revealDefinition to view one, mul, inv, mul_assoc, and mul_left_inv, but it doesn't work for one_mul and mul_one :thinking:

universe u

@[ext]
structure DirectProduct (α: Type u)[Group α] where
  fst : α
  snd : α

@[simp]
def dpMul{α : Type u}[Group α](d₁ d₂: DirectProduct α): DirectProduct α where
  fst := d₁.fst * d₂.fst
  snd := d₁.snd * d₂.snd

@[simp]
def dpInv{α : Type u}[Group α](d₁: DirectProduct α): DirectProduct α where
  fst := d₁.fst⁻¹
  snd := d₁.snd⁻¹

@[simp]
def dpOne{α : Type u}[Group α]: DirectProduct α where
  fst := 1
  snd := 1

variable{α : Type u}[Group α]
instance : Group (DirectProduct α) where
  one := dpOne
  mul := dpMul
  inv := dpInv
  mul_assoc := by sorry
  one_mul := by sorry
  mul_one := by sorry
  mul_left_inv := by sorry

3. Finally, I'm reading through some Lean tutorials like this one and there's mention of a lightbulb that will appear in VSCode if you start typing out a definition. I verified that "lightbulb" is enabled in my VSCode settings, but it doesn't appear when I start creating a definition for an instance of Group. How do you get it to show? Keeping with the Lean code above when I start typing

variable{α : Type u}[Group α]
instance : Group (DirectProduct α) where

I don't see anything particular interesting. It would be really cool to have it autofill with the fields so I can easily fill in all of the requisite fields to create an instance of Group for my custom type DirectProduct

[Ruben Van de Velde]

For 3, try writing := _ rather than where

[Noah Stebbins]

No dice. This is exactly what I'm seeing.

Screenshot-2024-07-07-at-12.42.41PM.png

[Ruben Van de Velde]

Doesn't that show the light bulb in the bottom left corner?

[Noah Stebbins]

Ok, yea I see the lightbulb now :+1:

[Marc Huisinga]

We don't implement the type hierarchy request (yet). The go-to-definition issue is worth reporting in the Lean 4 repository (with a Mathlib-free MWE that includes a minimized version of that part of the Group hierarchy).

[Noah Stebbins]

Gotcha any chance you know if a visual type hierarchy is supported in other IDEs like Neovim?

[Marc Huisinga]

No. This feature needs language server support, which we currently don't provide. Neither VS Code nor NeoVim can accurately compute this kind of information on their own.