Unexpanding nested structures

Stream: Is there code for X?

[Thomas Vigouroux]

Hey there.

I am trying to write an unexpander for a custom notation for a structure in my code, but I can't get it to work.

Here is a MWE:

structure Foo where
  a: Nat
  b: Nat

structure Bar where
  up: Nat
  inner: Foo

notation "F {" A "," B "," C "}"=> Bar.mk A (Foo.mk B C)

@[app_unexpander Bar.mk]
def Bar.unexp : Unexpander
| `($_ $up (Foo.mk $a $b)) => `(F {$up, $a, $b})
| _ => throw ()

example: F {1, 2, 3} = F {1, 2, 3} :=
by {
  -- Unexpand the notation here ?
}