replacing syntax node with `sorry`

Stream: lean4

[Jon Eugster]

I am trying to write a "tactic" Template that evaluates a tactic block, but also stores a (string) version of this tactic block, where all Holes are replaced with sorry so it can be used as a template later. But I'm struggling to create a sorry syntax node. #mwe:

open Lean

partial
def replaceHoles (tacs : Syntax) : Syntax :=
  match tacs with
  | Syntax.node info kind args =>
    match kind with
    | `GameServer.Tactic.Hole =>
      -- Replace the hole with a sorry.
      dbg_trace "got one!"
      -- TODO: How do I create a `sorry` syntax node?
      Syntax.node info `Lean.Parser.Tactic.tacticSorry #[]
    | k =>
      -- Iterate over the `args` to search for holes in there
      let newArgs := args.map <| (replaceHoles ·)
      Syntax.node info k newArgs
  | other =>
    -- Don't do anything to other syntax
    other

1. how do I create the sorry syntax at the TODO? (i.e. what should I put instead of #[]?
2. Is there a better way to do this? In particular I'd need to show termination for this kind of approach...

Expected Behaviour

The tactic block will look like this:

Template
  simp
  rw [h]
  Hole
    dsimp
    apply my_lemma
  assumption

and eventually I'd need to get a String that looks like

simp
rw [h]
sorry
assumption

to display it.

[Alex J. Best]

You can use check statements like #check `(command| theorem a : Nat := by sorry) to see what the syntax of a given command, idk if there is a better way but this works at least. So it seems you want #[Syntax.atom info "sorry"]

[Jon Eugster]

Oh thanks! I tried to dbg_trace it, but didn't realise that it was an .atom instead of a .node, so the outputs didn't make sense.