Skip to content

feat(Foundations/Semantics/ReductionSystem): extend ReductionSystem #304

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
Open
IvanRenison wants to merge 5 commits into
base: main
Choose a base branch
from
Open

feat(Foundations/Semantics/ReductionSystem): extend ReductionSystem #304

IvanRenison wants to merge 5 commits into from
+204 −56

Conversation

@IvanRenison
Copy link
Contributor

@IvanRenison IvanRenison commented Jan 30, 2026 •
edited
Loading

  • Add more definitions and theorems about reduction systems
  • Use namespace ReductionSystem
  • Add sections

@chenson2018
Copy link
Collaborator

chenson2018 commented Jan 30, 2026

Please add a description to this PR.

chenson2018
chenson2018 requested changes Jan 30, 2026
View reviewed changes
@IvanRenison IvanRenison changed the title feat(Foundations/Semantics/ReductionSystem): add more definitions and theorems about reduction systems, use namespace ReductionSystem, and add sections feat(Foundations/Semantics/ReductionSystem): extend ReductionSystem Jan 31, 2026
@IvanRenison
Copy link
Contributor Author

IvanRenison commented Jan 31, 2026

Should I also add the Convergent things to Relation?

@chenson2018
Copy link
Collaborator

chenson2018 commented Jan 31, 2026

Should I also add the Convergent things to Relation?

Yes. For the moment I would add it as an abbrev that is the conjunction of the two conditions. (We might revisit this later, but let's start with this for consistency)

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

Reviewers

@fmontesi fmontesi Awaiting requested review from fmontesi fmontesi is a code owner

@chenson2018 chenson2018 Awaiting requested review from chenson2018 chenson2018 is a code owner

Requested changes must be addressed to merge this pull request.

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@IvanRenison @chenson2018