Stream: lean4

Topic: modeling "simple" recursive datatypes

Zygimantas Straznickas (Feb 28 2021 at 17:28):

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.

Last updated: May 07 2021 at 13:21 UTC