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

Remove all nested/mutual inductives in favour of indexed dependent inductives

Open bollu opened this issue 3 years ago • 0 comments

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

bollu avatar Feb 08 '23 05:02 bollu