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

Bounded lists as explicit enumerations #1

Open
RandallYe opened this issue Jul 23, 2021 · 1 comment
Open

Bounded lists as explicit enumerations #1

RandallYe opened this issue Jul 23, 2021 · 1 comment
Assignees
@simondfoster
Labels
enhancement New feature or request

Comments

@RandallYe
Copy link
Collaborator

A bounded list for a finite type is enumerable. It is nice to have bounded lists as instances of the enum class, then we can access the explicit enumerations of a bounded list through T_enum.
@RandallYe RandallYe added the enhancement New feature or request label Jul 23, 2021
@RandallYe
Copy link
Collaborator Author

@simondfoster I saw you have an instantiation for enum. Now there is another issue for code generation. The following code in Isabelle

value "enum_class.enum:: (Chemical_Angle blist[2]) list"

will lead to an error: No code equations for blist_of_list

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@simondfoster simondfoster

Labels
enhancement New feature or request
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@simondfoster @RandallYe