Skip to content

refactor: SN adjacent to Terminating - #859

Open
lengyijun wants to merge 1 commit into
leanprover:mainfrom
awesome-lambda-calculus:snAcyclic
Open

refactor: SN adjacent to Terminating#859
lengyijun wants to merge 1 commit into
leanprover:mainfrom
awesome-lambda-calculus:snAcyclic

Conversation

@lengyijun

@lengyijun lengyijun commented Sep 3, 2026

Copy link
Copy Markdown
Contributor

No description provided.

@lengyijun lengyijun changed the title refactor: Move Acyclic to top for alphabetical ordering refactor: let SN adjacent to Terminating Sep 3, 2026
@lengyijun lengyijun changed the title refactor: let SN adjacent to Terminating refactor: SN adjacent to Terminating Sep 3, 2026
@lengyijun

Copy link
Copy Markdown
Contributor Author

@SamuelSchlesinger Could you take a look at this and let me know what you think?

@thomaskwaring

Copy link
Copy Markdown
Collaborator

this seems sensible to me, but the order of the definitions probably needs an overhaul anyway (eg moving the Commute and Confluent defs together) — i'm planning to do this along with some other shuffling around in Relation/* after #855 is merged, but that needn't stop this from going through.

@SamuelSchlesinger

Copy link
Copy Markdown
Collaborator

Fine with me.

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.

3 participants