Round trip elaboration

Stream: lean4

[Yakov Pechersky]

What is the current approach to proving that the defined elaboration and delaboration round trip successfully? In other words, how does one right the theorem that in the following example, elaborating and delaborating C : term gives the same output? Or that delaborating and elaborating C : atom gives the same value?

open Lean PrettyPrinter

inductive atom
| carbon | nitrogen | oxygen

syntax "C" : term
syntax "N" : term
syntax "O" : term

macro_rules
  | `(C) => `(atom.carbon)
  | `(N) => `(atom.nitrogen)
  | `(O) => `(atom.oxygen)

@[appUnexpander atom.carbon]
def unexpandCarbon : Unexpander
| `($(_)) => `(C)
| _       => unreachable!

@[appUnexpander atom.nitrogen]
def unexpandNitrogen : Unexpander
| `($(_)) => `(N)
| _       => unreachable!

@[appUnexpander atom.oxygen]
def unexpandOxygen : Unexpander
| `($(_)) => `(O)
| _       => unreachable!