Interpolation in comments

Stream: lean4

[Siddhartha Gadgil]

Can someone help with the correct way to do this:

def mkTheoremWithDoc (name: Name)(type: Syntax.Term)
    (doc: String) :
        CoreM String := do
    let name := mkIdent name
    let stx ← `(command|/-- $doc -/
    theorem $name : $type := by sorry)
    let fmt ← ppCategory `command stx
    return fmt.pretty

The problem is that $doc is taken as part of a comment, so ignored. I can make a separate string for the comment, but it seems aesthetically better to tell Lean what I mean.

To clarify, I got a warning that the variable doc is never used. I did not actually test.

[Damiano Testa]

It is unused, since it uses the literal text /-- $doc -/ as its doc.

[Damiano Testa]

Oh, you already discovered this!

[Siddhartha Gadgil]

Yes, I am asking if there is a way to make it be used.

[Damiano Testa]

This seems to work:

def mkTheoremWithDoc (name: Name)(type: Syntax.Term)
    (doc: String) :
        CoreM String := do
    let name := mkIdent name
    let docs := mkNode ``Lean.Parser.Command.docComment #[mkAtom "/--", mkAtom (doc ++ " -/")]
    let stx ← `(command| $docs:docComment theorem $name : $type := by sorry)
    let fmt ← ppCategory `command stx
    return fmt.pretty

[Siddhartha Gadgil]

Thanks.