Closed YaelDillies closed 1 month ago
This paragraph was written before the advent of reviewers.
The base of the PR needed to be lean4 rather than master, and when I changed it Github closed the PR and won't let me reopen. I will make a new copy now and merge. :-(
lean4
master
This paragraph was written before the advent of reviewers.