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

Split Calculus.lean into separate files #43

Merged
merged 5 commits into from
Jul 28, 2024
Merged

Split Calculus.lean into separate files #43

merged 5 commits into from
Jul 28, 2024

Conversation

Anatolay
Copy link
Collaborator

@Anatolay Anatolay commented Jun 18, 2024

Split Calculus.lean into several files and directories:

  • Term for definition of \phi-terms,
  • Reduction.Parallel for the definition and properties of parallel reduction,
  • Reduction.Regular for the definition and proof of confluence for regular reduction.

Also added Takahashi's technique to ARS.lean


PR-Codex overview

The focus of this PR is to introduce new theorems, definitions, and enhancements related to parallel reduction and record manipulation in the Lean codebase.

Detailed summary

  • Added a new theorem notEqByListMem in Utils.lean
  • Defined regular reduction in Reduction/Regular/Definition.lean
  • Introduced new properties and theorems related to reduction in ARS.lean
  • Added record manipulation definitions in Record.lean
  • Defined parallel reduction and related properties in Reduction/Parallel/Definition.lean
  • Implemented substitution lemma for parallel reduction in Reduction/Parallel/Substitution.lean

The following files were skipped due to too many changes: Minimal/Reduction/Parallel/Substitution.lean, Minimal/Reduction/Parallel/AuxilaryProperties.lean, Minimal/Reduction/Regular/Confluence.lean, Minimal/Reduction/Parallel/Confluence.lean, Minimal/Term.lean

✨ Ask PR-Codex anything about this PR by commenting with /codex {your question}

@Anatolay Anatolay merged commit e84e0e0 into master Jul 28, 2024
2 checks passed
@0crat
Copy link

0crat commented Jul 28, 2024

@Anatolay Thanks for the contribution! You've earned +5 points for this: +20 as a basis; +5 for 2053 hits-of-code; -7 for too many hits-of-code (2053 >= 100); -15 for way too many hits-of-code (2053 >= 400); -5 for 0 comments of reviewers; +7 to give you at least something. Please, keep them coming.

@eyihluyc eyihluyc deleted the separate-files branch August 6, 2024 15:02
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.

4 participants