Reflecting recursive types

Stream: lean4

[Jakob von Raumer]

Jakob von Raumer said:

I'm trying to reflect a class of recursive types in a language with a type system close to the one of C into Lean types, does anyone know if there's any projects doing a similar thing already? For examples, embedded mu calculus expressions as well as a implmentation to quote them into lean types?