lean-mlir icon indicating copy to clipboard operation
lean-mlir copied to clipboard
verified publisher icon opencompl

Full coinductive ITrees (Coitree)

Open bollu opened this issue 3 years ago • 5 comments

This patch sequence lays out the implementation of Coitrees. The sorrys are intentional, and will be merged into mainline once @lephe and @math-fehr review the PR to ensure that it's sensible.

bollu avatar Sep 24 '22 19:09 bollu

LGTM, thanks!

bollu avatar Jun 19 '23 01:06 bollu