Skip to content

TableOfContents.md: mention rami3l/PLFaLean as a derived work#1109

Merged
wenkokke merged 1 commit intoplfa:devfrom
rami3l:patch-1
Apr 9, 2025
Merged

TableOfContents.md: mention rami3l/PLFaLean as a derived work#1109
wenkokke merged 1 commit intoplfa:devfrom
rami3l:patch-1

Conversation

@rami3l
Copy link
Copy Markdown
Contributor

@rami3l rami3l commented Apr 8, 2025

Closes rami3l/PLFaLean#15.

As proposed in that very issue, this PR adds rami3l/PLFaLean as a derived work of PLFA.

@wadler Many thanks again for your appreciation!

@wenkokke
Copy link
Copy Markdown
Collaborator

wenkokke commented Apr 8, 2025

Could you add a short sentence describing which version or commit your work is based on and which chapters you've translated?

@wadler
Copy link
Copy Markdown
Member

wadler commented Apr 8, 2025

@wenkokke Better to have incomplete information now than perfect information later, so I've hit "merge" for this.

@rami3l Thank you. Please do add the sentence suggested by Wen in a later pull request. I'm currently writing a book based on PLFA, but with Lean in place of Agda and appropriate changes to the text. I was going to use PLFL for my book, so could I ask you to choose a different name for your repository? Perhaps PLFA-in-Lean?

@rami3l
Copy link
Copy Markdown
Contributor Author

rami3l commented Apr 8, 2025

I'm currently writing a book based on PLFA, but with Lean in place of Agda and appropriate changes to the text. I was going to use PLFL for my book, so could I ask you to choose a different name for your repository? Perhaps PLFA-in-Lean?

@wadler Thanks for letting me know! That said, I don't believe my personal exercise will really constitute a name conflict with your upcoming org, repo and/or book. If anything, I'd love to change the name of my repo to e.g. PLFaLean (so that it is clearly a PLFA derived work and has nothing to do with your new book), but I'd prefer to leave the project itself intact (the code is considered frozen so I'm a bit reluctant to change anything). How does that sound to you?

Could you add a short sentence describing which version or commit your work is based

@wenkokke Sorry, but I'm a bit confused right now because I'm not aware of any "version"s of this book. Has anything changed significantly since my finishing this project in 2023?

PS: If you are talking about GitHub releases, then it'll be https://github.com/plfa/plfa.github.io/releases/tag/v22.08, it seems to me.

@rami3l rami3l changed the title TableOfContents.md: mention rami3l/plfl as a derived work TableOfContents.md: mention rami3l/PLFaLean as a derived work Apr 8, 2025
@rami3l
Copy link
Copy Markdown
Contributor Author

rami3l commented Apr 8, 2025

I have made the said changes and would like to re-request a review from both @wenkokke and @wadler. Many thanks to both of you in advance!

@wenkokke wenkokke enabled auto-merge April 9, 2025 05:18
@wenkokke wenkokke added this pull request to the merge queue Apr 9, 2025
Merged via the queue into plfa:dev with commit 522a093 Apr 9, 2025
12 checks passed
@rami3l rami3l deleted the patch-1 branch April 9, 2025 07:49
noughtmare pushed a commit to noughtmare/plfa.github.io that referenced this pull request Oct 24, 2025
…#1109)

Closes rami3l/PLFaLean#15.

As proposed in that very issue, this PR adds `rami3l/PLFaLean` as a
derived work of PLFA.

@wadler Many thanks again for your appreciation!
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.

PLFA and PLFL

3 participants