Earlier quoted context omitted.
I'm not an expert in this field, but the way I understand it is that Choice Trees extend the ITree signature by adding a choice operator. Some variant of this: ITrees: CoInductive itree (E : Type -> Type) (R : Type) : Type := | Ret (r : R) | Tau (t : itree E R) | Vis {T : Type} (e : E T) (k : T -> itree E R) ChoiceTrees: CoInductive ctree (E : Type -> Type) (C : Type -> Type) (R : Type) : Type := | Ret (r : R) | Tau…
Ooooh! Those indeed look fun! :)
There are some issues arising from size inconsistencies (AKA Cantor's Paradox) if / when you try to fit the representation of all internal choices (this could be infinite) into a small universe of a theorem prover's inductive types. The ChoiceTree paper solves this with a specific encoding. I'm currently wondering how to port this trick from COq/Rocq to Lean4.