lean-mlir
lean-mlir copied to clipboard
opencompl
wip: prototype zext/sext extensions for automata/k-induction
This PR prototypes the reflection we would need to do for multiple widths, and also proves correct the on-paper reduction of zext and sext for finite automata.
![github-actions[bot] avatar](https://avatars.githubusercontent.com/in/15368?v=4 "Published by a pub.dev verified publisher"){kind=small}