Skip to content
This repository has been archived by the owner on Jun 17, 2024. It is now read-only.

Typed syntax #25

Open
2 tasks
lephe opened this issue Jul 4, 2022 · 0 comments
Open
2 tasks

Typed syntax #25

lephe opened this issue Jul 4, 2022 · 0 comments
Assignees
@bollu

Comments

@lephe
Copy link
Contributor

lephe commented Jul 4, 2022

opencompl/lean-mlir@cf7d682 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
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Assignees

@bollu bollu

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@bollu @lephe