What is `term.pseudo.antiquot`?

Stream: lean4

[Leni Aniva]

Printing out the syntax tree of Mathlib/ModelTheory/Syntax.lean, I found this constant

           (Tactic.refine
            "refine"
            (Mathlib.Tactic.TermCongr.termCongr
             "congr("
             (Set.term_''_
              (Term.hole "_")
              "''"
              (Term.paren
               "("
               («term_∩_»
                (term.pseudo.antiquot "$" [] (antiquotNestedExpr "(" (Term.syntheticHole "?" "_") ")") [])
                "∩"
                (Term.hole "_"))
               ")"))
             ")"))

which occurs on this line:

    refine ⟨fun h => ⟨{⟨i, h.1⟩, ⟨j, h.2⟩}, ⟨h.1, ?_⟩, ⟨h.2, ?_⟩⟩, ?_⟩

what is term.pseudo.antiquot? The Lean tactic prettyprinter fails to print this

[Eric Wieser]

I think you have the line number wrong

[Eric Wieser]

It should be from something like exact congr(_ '' ($(?_) \inter _)

[Mario Carneiro]

refine congr(_ '' ($(?_) ∩ _))

[Mario Carneiro]

the answer to your question is that term.pseudo.antiquot is the syntax for antiquotations, which for no particularly good reason has no pretty printer. (I think this narrowly avoided being an issue for mathport because lean 3 did not have congr(...) or q(...) and we did not attempt to translate tactic metaprograms containing antiquotations)

[Mario Carneiro]

cc: @Sebastian Ullrich

[Leni Aniva]

Mario Carneiro said:

the answer to your question is that term.pseudo.antiquot is the syntax for antiquotations, which for no particularly good reason has no pretty printer. (I think this narrowly avoided being an issue for mathport because lean 3 did not have congr(...) or q(...) and we did not attempt to translate tactic metaprograms containing antiquotations)

Should I write a prettyprinter for it and pr?

[Sebastian Ullrich]

I don't think it is quite trivial to implement it in full antiquotation generality. Might be better to implement a local pretty printer in your project specifically for your use case.

[Eric Wieser]

Could it print as $<cannot print> or something to prevent it tainting the entire syntax being printed?

[Mario Carneiro]

I think that's a general suggestion too, although IIRC this is hard to implement because the formatter misuses backtracking so it can't tell the difference between missing formatters and deliberate alternation