lean-mlir
lean-mlir copied to clipboard
opencompl
embedding MLIR in LEAN
The hope is that this eliminates the huge terms from `WellFounded.fix` and the massive performance slowdown we see along the way.
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
@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...
https://github.com/opencompl/lean-mlir/commit/cf7d6828ef52a54339a2dc7aa6345bfd4d56c274 updates to a nightly after the implementation of typed syntax. It enriches the types in some places but mostly adds bypasses, and some of these reveal parsing errors I...
The EDSL is now more powerful, and keeping both systems with different parsing power seems like it could be a problem in the longer run (and I don't think you...
There are currently two sorries in the file `BitStream.lean`. This proof removes one sorry, in the case of addition by proving that addition on BitVectors agrees with addition on BitStreams...
