Skip to content

refactor(LocallyNameless/Untyped): rename close_open => close_openRec - #678

Open
lengyijun wants to merge 3 commits into
leanprover:mainfrom
awesome-lambda-calculus:close_openRec
Open

refactor(LocallyNameless/Untyped): rename close_open => close_openRec#678
lengyijun wants to merge 3 commits into
leanprover:mainfrom
awesome-lambda-calculus:close_openRec

Conversation

@lengyijun

@lengyijun lengyijun commented Jun 24, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor
  • open_close → open_closeRec (general)
  • open_close_var → open_close (k = 0)
  • close_open → close_openRec (general)
  • add specialized close_open

First part of #860

@chenson2018 chenson2018 self-assigned this Jul 5, 2026
@lengyijun lengyijun mentioned this pull request Sep 3, 2026
Open
@lengyijun
lengyijun force-pushed the close_openRec branch 2 times, most recently from 4cbb4b7 to b2acf99 Compare September 21, 2026 23:46
@lengyijun
lengyijun force-pushed the close_openRec branch 3 times, most recently from e4798ca to dbf89c3 Compare September 28, 2026 00:14
@lengyijun
lengyijun force-pushed the close_openRec branch 2 times, most recently from 4cb6c3e to 411bc4c Compare October 5, 2026 00:28
@lengyijun
lengyijun requested a review from crei as a code owner October 5, 2026 00:28
SamuelSchlesinger
SamuelSchlesinger requested changes Oct 10, 2026
View reviewed changes

@SamuelSchlesinger SamuelSchlesinger left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

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

This looks related to #860, can you mention that in the description potentially?

Comment thread Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Properties.lean
Comment thread Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Properties.lean
@SamuelSchlesinger

SamuelSchlesinger commented Oct 11, 2026

Copy link
Copy Markdown
Collaborator

cc @chenson2018

@lengyijun
refactor(LocallyNameless/Untyped): rename close_open => close_openRec
b53f928 
- Rename the general version with explicit depth `k` into `close_openRec`
- Introduce a new theorem for `k = 0` : `close_open`
@lengyijun
doc
f1534bb
@lengyijun
open_closeRec
c79b2cf
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@chenson2018 chenson2018 Awaiting requested review from chenson2018 chenson2018 is a code owner
@fmontesi fmontesi Awaiting requested review from fmontesi fmontesi is a code owner
@kim-em kim-em Awaiting requested review from kim-em
@arademaker arademaker Awaiting requested review from arademaker arademaker is a code owner
@sorrachai sorrachai Awaiting requested review from sorrachai sorrachai is a code owner
@crei crei Awaiting requested review from crei crei is a code owner
@SamuelSchlesinger SamuelSchlesinger Awaiting requested review from SamuelSchlesinger SamuelSchlesinger is a code owner

Requested changes must be addressed to merge this pull request.

Assignees

@chenson2018 chenson2018

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@lengyijun @SamuelSchlesinger @chenson2018