When you hover over code in Lean, it shows some information: Hovering over a string (That’s the result of me hovering over the text "hi" in this example command. It shows that its type is a String.)

I can modify what I do in the code defining #test and change what the hover says: The hover now shows different text I think that’s pretty neat.

How is this possible?

When you hover over something, some program is called whose job is to return the information about the text you are hovering above. That program needs to know what all the code in the file means in order to say what the type information is.

Lean’s metaprogramming means that in a Lean file we can control what a piece of syntax means. And thus, we control the hovers!

An example

Let’s see an example. Try hovering yourself in the online editor.

import Lean

elab "#test " e:term : command => return ()

#test "hi"

Here we define a new piece of syntax #test that takes in one argument e and overall it is a command. And then we provide what that code means, which here is nothing.

So on the next line #test "hi" does nothing. And when you hover over it, nothing is displayed because that code has no meaning. Even though it may look like "hi" is a string, it has no hover because we gave this code no meaning.

Now let’s give "hi" its normal meaning. Lean calls the process of giving code meaning elaboration. So we are going to elaborate e. Online editor

import Lean
open Lean Elab Command Term

elab "#test " e:term : command => liftTermElabM do
  let _ ← elabTerm e none

#test "hi"

Since we have called elabTerm e none, we can now hover over "hi" and see that its type is a String.

Let’s make it so that hovering over "hi" shows instead what would happen if we were hovering over 5. Online editor

import Lean
import Qq
open Lean Elab Term Command Qq

elab "#test " e:term : command => liftTermElabM do
  addTermInfo' e q(5)

#test "hi"

And when we hover over "hi" we now see the following: Hover now shows information for the number `5`

What’s going on in this code? The program that handles the hover information is specifically getting information from what is called the InfoTree. We can add hover information to this tree with the function addTermInfo'. Here we said that the syntax e has the information for 5. And thus our hover shows 5 : Nat!

In more complicated code, the InfoTree is gradually built up as code is given meaning during elaboration. Since this example was simple, we were able to just make the InfoTree what we wanted it to be in one go.