Zulip Chat Archive

Stream: lean4

Topic: modeling "simple" recursive datatypes

view this post on Zulip 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