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

Convert literal naturals to Nat terms #1645

Closed
jonaprieto opened this issue Nov 22, 2022 · 1 comment · Fixed by #1681
Closed

Convert literal naturals to Nat terms #1645

jonaprieto opened this issue Nov 22, 2022 · 1 comment · Fixed by #1681
Assignees

Comments

@jonaprieto
Copy link
Collaborator

No description provided.

@jonaprieto jonaprieto added this to the 0.3 milestone Nov 22, 2022
@lukaszcz
Copy link
Collaborator

lukaszcz commented Dec 12, 2022

Just converting literal naturals to Nat terms will be terribly inefficient. We should have a builtin function intToNat in the core (an identifier with a definition, marked as builtin intToNat), and at first convert a literal natural X to intToNat X, and then when converting Nat representation to Core integers change all applications intToNat X to X and all other occurrences of intToNat to identity.

@lukaszcz lukaszcz self-assigned this Dec 22, 2022
jonaprieto added a commit that referenced this issue Jan 3, 2023
Now it's possible to write `1 + 2` in the Juvix REPL and not get an
error.

Closes #1645.

Co-authored-by: Jonathan Cubides <jonathan.cubides@uib.no>
janmasrovira pushed a commit that referenced this issue Jan 3, 2023
Now it's possible to write `1 + 2` in the Juvix REPL and not get an
error.

Closes #1645.

Co-authored-by: Jonathan Cubides <jonathan.cubides@uib.no>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants