Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

LLVM backend: add support for uset #1958

Closed
bollu opened this issue Dec 16, 2022 · 0 comments · Fixed by #2025
Closed

LLVM backend: add support for uset #1958

bollu opened this issue Dec 16, 2022 · 0 comments · Fixed by #2025
Milestone

Comments

@bollu
Copy link
Contributor

bollu commented Dec 16, 2022

The LLVM backend (#1837) does not implement uset, as no test case in the Lean4 test suite produces a uset. Add a test that produces a uset, and generate the right code for it. A potential test case is:

structure Point where
  x : USize
  y : UInt32

@[noinline] def Point.right (p : Point) : Point :=
  { p with x := p.x + 1 }

def main : IO Unit :=
  IO.println (Point.right ⟨0, 0⟩).x
@Kha Kha added this to the LLVM MVP milestone Dec 16, 2022
bollu added a commit to bollu/lean4 that referenced this issue Jan 9, 2023
bollu added a commit to bollu/lean4 that referenced this issue Jan 9, 2023
@Kha Kha closed this as completed in #2025 Jan 9, 2023
Kha pushed a commit that referenced this issue Jan 9, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants