Custom Deriving for Serialization Library

Stream: metaprogramming / tactics

[Oliver Dressler]

I have been working on a serialization library which should support many custom structures.
Lean Metaprogramming is not my specialty, and I have arrived at this code for deriving after lots of trial and error:
https://github.com/oOo0oOo/LeanSerial/blob/main/LeanSerial/Derive.lean
(Sorry, I can't paste the code directly as the 300 LOC are too long)

My questions are:

• Is this code brittle and likely to break in practice?
• Which reasonable extensions are missing to support more structures?

Thanks for your support!