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.

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

feat: allow configuring occs in rw #2470

Merged
merged 1 commit into from
Sep 13, 2023
Merged

feat: allow configuring occs in rw #2470

merged 1 commit into from
Sep 13, 2023

Conversation

kim-em
Copy link
Collaborator

@kim-em kim-em commented Aug 28, 2023

This PR:

  • allows specifying occs in the config for rw
  • moves Occurrences so that this is possible
  • documents the current behaviour of occurrences (at the first match, whether allowed or not by occurrences, the metavariables in the rewrite will be instantiated, determining which subsequent matches are possible).

(In a future change I would like to propose changing this behaviour: i.e. at excluded occurrences, roll back the metavariable context so different matches can still be found. But best to keep this separate.)

@kim-em kim-em changed the title feat: rw with occs, and improve occs behavior feat: allow configuring occs in rw Aug 28, 2023
@kim-em kim-em marked this pull request as draft August 28, 2023 12:05
@kim-em kim-em marked this pull request as ready for review August 29, 2023 04:00
@kim-em kim-em added the awaiting-review Waiting for someone to review the PR label Aug 29, 2023
@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Sep 12, 2023
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Sep 12, 2023
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#2470
20b1a0e
@leanprover-community-mathlib4-bot
Copy link
Collaborator

leanprover-community-mathlib4-bot commented Sep 12, 2023 •
edited
Loading

@leodemoura leodemoura merged commit c318d58 into leanprover:master Sep 13, 2023
kim-em added a commit that referenced this pull request Sep 15, 2023
@kim-em
chore: add release notes for #2470 and #2480
72c39ec
kim-em added a commit to kim-em/lean4 that referenced this pull request Sep 15, 2023
@kim-em
chore: add release notes for leanprover#2470 and leanprover#2480
7db2e83
kim-em added a commit that referenced this pull request Sep 17, 2023
@kim-em @tydeu
chore: begin development cycle for 4.2.0 (#2545)
26de6d3 
* chore: add release notes for #2470 and #2480

* chore: begin development cycle for 4.2.0

* chore: add Lake-related release notes for v4.1.0

---------

Co-authored-by: Mac Malone <tydeu@hatpress.net>
0x450x6c pushed a commit to 0x450x6c/lean4 that referenced this pull request Oct 22, 2023
@kim-em
chore: add release notes for leanprover#2470 and leanprover#2480
0916968
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees

@leodemoura leodemoura

Labels
awaiting-review Waiting for someone to review the PR toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@kim-em @leanprover-community-mathlib4-bot @leodemoura