lean-mlir icon indicating copy to clipboard operation
lean-mlir copied to clipboard

Typed syntax

Open lephe opened this issue 2 years ago • 0 comments

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 believe.

  • [ ] Review the places where the commit trusts the types
  • [ ] Fix the typing issues that arise

lephe avatar Jul 04 '22 13:07 lephe