mathlib3
[Merged by Bors] - doc: Add a warning mentioning Lean 4 to the readme
#19243
Closed
Overview
Commits
2
Changes
View On GitHub

[Merged by Bors] - doc: Add a warning mentioning Lean 4 to the readme #19243

eric-wieser wants to merge 2 commits into master from eric-wieser/readme-admonition
eric-wieser
eric-wieser doc: Add a warning mentioning Lean 4 to the readme
6cc82e33
eric-wieser A few more
c78894c9
eric-wieser eric-wieser requested a review from digama0 digama0 2 years ago
eric-wieser eric-wieser added docs
eric-wieser eric-wieser added not-too-late
PatrickMassot
github-actions github-actions added ready-to-merge
bors
bors bors changed the title doc: Add a warning mentioning Lean 4 to the readme [Merged by Bors] - doc: Add a warning mentioning Lean 4 to the readme 2 years ago
bors bors closed this 2 years ago
bors bors deleted the eric-wieser/readme-admonition branch 2 years ago

Login to write a write a comment.

Login via GitHub

Reviewers
Assignees
No one assigned
Labels
ready-to-merge docs not-too-late
Milestone
No milestone
Terms Of Use Privacy Policy Refund Policy Impressum