Convert inductive into computation

Stream: Is there code for X?

[Zhuanhao Wu]

Do we have something like this for lean4, or is someone working on this?
https://lemonidas.github.io/pdf/ComputingCorrectly.pdf

Essentially it can convert relations such as A -> A -> Prop into some function A -> m A (with monad for simulating non-determinism) , so that a user can "execute" the relation.