David Thrane Christiansen 5d91ed01b7 doc: review String docstrings (#7506) ... This PR adds missing `String` docstrings and makes the existing ones consistent in style.		2025-03-18 04:36:49 +00:00
..
Basic.lean	doc: review String docstrings (#7506)	2025-03-18 04:36:49 +00:00
Extra.lean	doc: review String docstrings (#7506)	2025-03-18 04:36:49 +00:00
Lemmas.lean	feat: lemmas about List/Array/Vector lexicographic order (#6423)	2024-12-20 06:16:27 +00:00