What exactly are double backticks

Stream: lean4

[Hanting Zhang]

Hi, I'm getting started with Lean 4 but I have no idea what I'm doing. The Metaprogramming Book was very helpful in getting me started, but I'm still confused on some things. Is there any reference that explains exactly how quotations/antiquotations/quasiquotations work in Lean? Why is mkConst ``zero understood as mkConst `Nat.zero? Is `` a singular operation or two quotes nested together?

[Hanting Zhang]

Also how do I escape a backtick (so I can write mkConst Nat.zero`)

[Arthur Paulino]

Escaping example: `escaped!

You can "View source" on this message :+1:

[Sebastian Ullrich]

There is a little docstring if you hover over the `` in the editor

[Alex J. Best]

The single backtick is used to write a name, and a double backtick is used to write a name that is checked to currently be in the environment:

#check `Nat -- works
#check ``Nat -- works
#check `Cat -- works
#check ``Cat -- fails

[Hanting Zhang]

Sebastian Ullrich said:

There is a little docstring if you hover over the `` in the editor

Oh, when you hover over ``Nat it generates a docstring that's labelled with `Nat: [...], so I thought it was talking about a single quote, oops

[Hanting Zhang]

But I think I get it now!

[Mario Carneiro]

The double backtick doesn't only do compile time checking of the name, it also does name resolution, which can change the actual name literal being used:

namespace Foo
def Cat := 1

#eval `Cat  -- `Cat
#eval ``Cat -- `Foo.Cat