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

Directly allow numbers as terms #74

Open
SReichelt opened this issue Aug 25, 2020 · 0 comments
Open

Directly allow numbers as terms #74

SReichelt opened this issue Aug 25, 2020 · 0 comments
Assignees
Labels
component: hlm logic Issue concerns the HLM logic

Comments

@SReichelt
Copy link
Owner

It should be possible to reference numbers directly without referring to $number. Instead, as already noted in #46, certain sets should specify how to interpret numbers as elements of that set, by referencing e.g. $number, $inverse, and $quotient (see below).

This would have several advantages:

Ideally, we want to extend this to integers and rational numbers (including decimal notation); see #46. The type of every number should be determined automatically.

However, we cannot remove the $number macro entirely because when a number appears without context, it is not clear how to interpret it.

Can we somehow extend this to arbitrary (semi)rings? It seems we would need to attach the information to $Carrier then.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
component: hlm logic Issue concerns the HLM logic
Projects
None yet
Development

No branches or pull requests

1 participant