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

Fix LEM instances and eta for product cubes #88

Merged

fizruk merged 3 commits into develop from fix-topes-LEM-eta

Sep 21, 2023

Member

fizruk commented Sep 21, 2023 •

edited

Loading

This PR contains two fixes, discovered in rzk-lang/sHoTT#30 (comment):

We now only generate well-typed LEM instances in the tope solver.
We fix $\eta$-rule for product cubes, to not get stopped by reflexive equality topes like $\langle \langle \pi_1 (t_{12}), \pi_2 (t_{12}) \rangle, t_3 \rangle \equiv \langle t_{12}, t_3 \rangle$.

fizruk added 3 commits

September 21, 2023 11:39


          Stop generating ill-typed LEM instances for topes

393a880


          Fix eta-rule for product cubes

b9a32d1


          Fix eta-rule again (works, but might not be complete)

91f4174

Member Author

fizruk commented Sep 21, 2023

I guess, this is evidence that the tope solve should be properly redesigned and reimplemented :)

fizruk merged commit f1597a1 into develop

2 checks passed

fizruk deleted the fix-topes-LEM-eta branch

September 21, 2023 13:41

fizruk mentioned this pull request

Release v0.5.7 #89

Merged

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

Labels

None yet