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

String and char literals #218

Closed
ice1000 opened this issue May 27, 2020 · 1 comment · Fixed by #232
Closed

String and char literals #218

ice1000 opened this issue May 27, 2020 · 1 comment · Fixed by #232
Assignees
Milestone

Comments

@ice1000
Copy link
Contributor

ice1000 commented May 27, 2020

We may support string and char literals, and make a non-builtin library for string manipulation (via language extension).

Pros:

  • Make it possible to write parsers and pretty printers in Arend (like agdarsec)
  • More flexible input to tactics -- we can pass some textual information
  • A step towards reflection API in Arend (accessing Arend AST in Arend -- in other words, quote/unquote)

Cons:

  • Conversion between string and char list is very common, but if we want to support this, we also want to prove that such conversion is an isomorphism. If we built-in this axiom, we need to built-in the list type
  • One more AST type for concrete and core
  • This has few things to do with theorem proving, which is the current major focus of Arend
ice1000 added a commit that referenced this issue Jul 6, 2020
@ice1000 ice1000 self-assigned this Jul 6, 2020
@ice1000 ice1000 added this to the 1.5 milestone Jul 6, 2020
@ice1000
Copy link
Contributor Author

ice1000 commented Jul 6, 2020

Strings can supersede chars. I'll finish strings

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.

1 participant