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

Cursor inspector now uses typ equality as opposed to full structural equality #1418

Draft
wants to merge 6 commits into
base: dev
Choose a base branch
from

Conversation

7h3kk1d
Copy link
Contributor

@7h3kk1d 7h3kk1d commented Nov 18, 2024

Old version
Screenshot from 2024-11-18 14-22-40
New version
Screenshot from 2024-11-18 14-23-22

Depends on #1409 for a notion of ID-unaware equality.

@cyrus-
Copy link
Member

cyrus- commented Nov 18, 2024

what happens with alpha equivalent types (e.g. forall x -> (x, x) and forall a -> (a, a))?

@7h3kk1d
Copy link
Contributor Author

7h3kk1d commented Nov 18, 2024

what happens with alpha equivalent types (e.g. forall x -> (x, x) and forall a -> (a, a))?

@cyrus- According to the docstring it should do alpha equivalence but not normalization. https://github.com/hazelgrove/hazel/blob/dev/src/haz3lcore/statics/TermBase.re#L693

If we don't want it for alpha equivalent types I can introduce a 3rd form of equality that just ignores IDs.

@7h3kk1d
Copy link
Contributor Author

7h3kk1d commented Nov 18, 2024

This may be a bug somewhere else as well though

Screenshot from 2024-11-18 14-44-16

@7h3kk1d 7h3kk1d marked this pull request as draft November 20, 2024 22:12
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants