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.

Sign up for GitHub

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

Jump to bottom

Concepts macro doesn't recognize names of Agda data types #1073

Closed
fredrik-bakke opened this issue Mar 14, 2024 · 1 comment · Fixed by #1074
Closed

Concepts macro doesn't recognize names of Agda data types #1073

fredrik-bakke opened this issue Mar 14, 2024 · 1 comment · Fixed by #1074
Labels
bug Something isn't working CI mathswitch

Comments

@fredrik-bakke
Copy link
Collaborator

I tried adding a concept macro for the coproduct type _+_, but this makes the CI throw an error.
@fredrik-bakke fredrik-bakke added bug Something isn't working CI labels Mar 14, 2024
@VojtechStep
Copy link
Collaborator

I don't think it's a problem of it not recognizing data types (the identity type works just fine), but that it doesn't escape the symbol's name when putting together the regex, so it interprets _+_ as two or more underscores.

@VojtechStep VojtechStep mentioned this issue Mar 14, 2024
Merged
VojtechStep added a commit that referenced this issue Mar 14, 2024
@VojtechStep
Escape Agda definitions when translating them to regex (#1074)
91aa283 
The concept macro looks for Agda definitions when the Agda= component is
specified. Until now the definition name was not escaped, so concepts
like the coproduct type `_+_` could not be found by the macro.

Fixes #1073
fredrik-bakke pushed a commit to fredrik-bakke/agda-unimath that referenced this issue Mar 14, 2024
@VojtechStep @fredrik-bakke
Escape Agda definitions when translating them to regex (UniMath#1074)
cd8adbe 
The concept macro looks for Agda definitions when the Agda= component is
specified. Until now the definition name was not escaped, so concepts
like the coproduct type `_+_` could not be found by the macro.

Fixes UniMath#1073
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
bug Something isn't working CI mathswitch
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Escape Agda definitions when translating them to regex VojtechStep/agda-unimath
2 participants
@fredrik-bakke @VojtechStep