modeling "simple" recursive datatypes

Stream: lean4

[Zygimantas Straznickas]

I'm implementing protobuffer support for lean4, and one interesting challenge is that the protobuf standard supports proto definitions with recursive type dependencies:

message A {
    optional A recursive_field = 1;
    optional B mutual_recursive_field = 2;
}

message B {
    optional A mutual_recursive_field = 1;
}

I could in theory kinda-sorta translate this to Lean using mutual induction but the ergonomics of using generated code would be awful. I wonder if it's possible (likely through custom codegen) to better support these kinds of structures with the restriction that all structure fields are "simple" - either data or optional references of other such structs.