unknown constant 'term.pseudo.antiquot'

Stream: lean4

[Eric Wieser]

Perhaps a contrived example, but the pretty printer struggles here:

import Lean

open Lean Meta

set_option trace.debug true
set_option pp.rawOnError true

#eval show MetaM _ from do
  trace[debug] "{← `(`($$x + 1))}"

which gives the output

[debug] [Error pretty printing syntax: unknown constant 'term.pseudo.antiquot'. Falling back to raw printer.]
    (Term.quot "`(" («term_+_» (term.pseudo.antiquot "$" [] `x._@.Qq.test._hyg.1 []) "+" (num "1")) ")")

[Eric Wieser]

It's not clear to me where term.pseudo.antiquot comes from in the first place, or how to teach the pretty printer how to print it

[Kyle Miller]

`(`($$x + 1)) evaluates to `($x + 1), and the term.pseudo.antiquot node refers to $x. I'm not sure what the state of pretty printing antiquotations is, whether it's supposed to work or if it's not implemented.

[Eric Wieser]

What does pseudo refer to here?

[Kyle Miller]

There are two constructors for antiquotes, docs#Lean.Syntax.mkAntiquotNode and docs#Lean.Parser.mkAntiquot, and the second mentions that pseudo indicates that the kind isn't checked in match expression patterns (but I'm not completely sure)

[Eric Wieser]

I guess don't really understand what "checked" means here

[Kyle Miller]

If you had the pattern $x:ident + 1, then it would want to check that x is referring to some syntax of kind ident, but in $x + 1 it doesn't care what syntax kind that x has. ("It" being "what the match expression compiles to".)

[Kyle Miller]

There's a separate elaborator for match expressions for syntax patterns in Lean.Elab.Quotation, and it looks like pseudo controls whether to insert Syntax.isOfKind checks.

[Eric Wieser]

Ah, that helps a bit; in that case, this is a second pretty-printer failure (now about ident.antiquot):

#eval show MetaM _ from do
  trace[debug] "{← `(`($$x:ident + 1))}"

[Eric Wieser]

So maybe antiquot printing is not implemented at all, which would explain why I couldn't find it