Skip to content

Implement interpolated string #1056

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

Merged
merged 9 commits into from
Feb 18, 2021
Merged

Implement interpolated string #1056

merged 9 commits into from
Feb 18, 2021

Conversation

andylokandy
Copy link
Contributor

@andylokandy andylokandy commented Feb 10, 2021

This PR implements both #1027 and #555, basing on #1034.

For example, the listing below equals to "Hello Idris2!":

let idris = "Idris" in 
  "Hello \{idris ++ show 2}!"

For more details see #1027.

@andylokandy andylokandy marked this pull request as draft February 10, 2021 19:39
@andrevidela
Copy link
Collaborator

we can probably close #1034 and focus on this PR

@andylokandy
Copy link
Contributor Author

@andrevidela Isn't it too large as a whole?

@andylokandy andylokandy marked this pull request as ready for review February 10, 2021 21:57
@buzden
Copy link
Collaborator

buzden commented Feb 11, 2021

we can probably close #1034 and focus on this PR

It seems that #1034 has its own separate value disregarding raw strings.

@andylokandy andylokandy changed the title Support dynamic raw string delimiter Implement interpolated string Feb 12, 2021
@andylokandy
Copy link
Contributor Author

andylokandy commented Feb 12, 2021

@gallais @andrevidela @ohad I've implemented the interpolated string and I reused this PR (originally for raw strings) for it since they are quite related IMO. 😄

Signed-off-by: Andy Lok <andylokandy@hotmail.com>
Signed-off-by: Andy Lok <andylokandy@hotmail.com>
Signed-off-by: Andy Lok <andylokandy@hotmail.com>
Copy link
Member

@gallais gallais left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

One last question

@gallais gallais merged commit 2646435 into idris-lang:master Feb 18, 2021
@andrevidela andrevidela mentioned this pull request Feb 18, 2021
3 tasks
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 this pull request may close these issues.

4 participants