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

Remove eqb => eq #1062

Open
bvssvni opened this issue May 11, 2021 · 2 comments
Open

Remove eqb => eq #1062

bvssvni opened this issue May 11, 2021 · 2 comments
Labels
discussion draft

Comments

@bvssvni
Copy link
Contributor

bvssvni commented May 11, 2021 •
edited
Loading

An alternative to adding a context solver is separating eqb and eq. This means eqb => eq must be removed. However, eq{(: bool), (: bool)} might be used instead.
@bvssvni
Copy link
Contributor Author

bvssvni commented May 11, 2021 •
edited
Loading

Could add eqb <=> eq{(: bool), (: bool)}.

This can be used as following to lift eq into eqb:

(a & b = c) <=> eq{(: bool), (: bool)}(a & b)(c)

bvssvni added a commit to bvssvni/poi that referenced this issue May 11, 2021
@bvssvni
Removed eqb => eq
709aa9f 
See advancedresearch#1062
@bvssvni bvssvni mentioned this issue May 11, 2021
Merged
@bvssvni
Copy link
Contributor Author

bvssvni commented May 12, 2021

One idea is to use <-> for eqb.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
discussion draft
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@bvssvni