Mario Carneiro c9e84a6ad6 fix: remove private from string defs		2023-05-05 12:09:38 -07:00
..
Basic.lean	fix: remove private from string defs	2023-05-05 12:09:38 -07:00
Extra.lean	doc: various String docstrings	2022-08-26 20:49:57 -07:00