You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
If you find an ornament between A and B, and then also find an ornament between C and D, where D depends on A, and try to forgetfully lift terms defined over packed D, you get a term that also tries to lift along the ornament from A at the same time. This is weird behavior.
An example is finding an ornament between nat and some other type, then forgetting from packed vectors. Forget will unfortunately try to promote nat at the same time.
The text was updated successfully, but these errors were encountered:
If you find an ornament between A and B, and then also find an ornament between C and D, where D depends on A, and try to forgetfully lift terms defined over packed D, you get a term that also tries to lift along the ornament from A at the same time. This is weird behavior.
An example is finding an ornament between nat and some other type, then forgetting from packed vectors. Forget will unfortunately try to promote nat at the same time.
The text was updated successfully, but these errors were encountered: