Siddharth

The hope is that this eliminates the huge terms from `WellFounded.fix` and the massive performance slowdown we see along the way.

Full coinductive ITrees (Coitree)

5

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

section 7.1.3 (Bitwise Tricks and Techniques) of volume 4A of The Art of Computer Programming: https://www-cs-faculty.stanford.edu/~knuth/fasc1a.ps.gz https://news.ycombinator.com/item?id=33278589

`TopM.get` always succeeds if dominance check passes

1

@math-fehr When we reason about `linalg.runRegion`, we want to show that we can safely reorder running of regions. - errors can be reordered with anything - `set` can be reordered...

It's nice to have a link to the paper pre-print so we don't need to go hunting for the explanation!

Krohn rhodes theory: cascade decomposition?

1

Would there be interest in including the cascade decomposition algorithm from [Krohn-Rhodes](https://en.wikipedia.org/wiki/Krohn%E2%80%93Rhodes_theory) theory into the library? I don't see it currently, but it seems like a very useful algorithm to...