Skip to content

Conversation

@strub
Copy link
Member

@strub strub commented Sep 24, 2024

No description provided.

@strub strub self-assigned this Sep 24, 2024
@strub strub force-pushed the user-red-with-projections branch from f8d6e67 to 19e5c09 Compare September 24, 2024 07:56
@strub strub changed the title User red with projections internals: user-defined rules can be headed by a projection Sep 24, 2024
@strub strub marked this pull request as ready for review September 24, 2024 12:11
Copy link
Member

@alleystoughton alleystoughton left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

See my comment on #613. Simplification already handles projections of tuples, so I guess what you've implemented so far doesn't add anything?

@strub strub force-pushed the user-red-with-projections branch 2 times, most recently from f18b1d0 to 2a59b58 Compare September 24, 2024 15:44
Copy link
Member

@alleystoughton alleystoughton left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks good!

This commit also fixes some incompleteness in the CBV reduction
strategy w.r.t. user rules.
@strub strub force-pushed the user-red-with-projections branch from 2a59b58 to ab542c9 Compare September 24, 2024 16:22
@strub strub merged commit 287015d into main Sep 24, 2024
@strub strub deleted the user-red-with-projections branch September 24, 2024 16:46
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

anomaly with hint simplify [reduce] for equational lemma involving projection

3 participants