max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/src/Init/System
History
David Thrane Christiansen 1b0168d7b3
doc: docstring review for System and System.FilePath (#7523) 
This PR adds missing docstrings and makes docstring style consistent for
`System` and `System.FilePath`.
2025-03-19 05:14:35 +00:00
..
FilePath.lean doc: docstring review for System and System.FilePath (#7523) 2025-03-19 05:14:35 +00:00
IO.lean doc: docstring review for System and System.FilePath (#7523) 2025-03-19 05:14:35 +00:00
IOError.lean doc: review docstrings for IO (#7476) 2025-03-17 17:59:44 +00:00
Mutex.lean refactor: move IO.Channel and IO.Mutex to Std.Sync (#6282) 2024-12-03 09:36:50 +00:00
Platform.lean doc: docstring review for System and System.FilePath (#7523) 2025-03-19 05:14:35 +00:00
Promise.lean fix: never transfer constants from checked environment into elab branches (#7306) 2025-03-05 17:12:27 +00:00
ST.lean doc: review docstrings for IO (#7476) 2025-03-17 17:59:44 +00:00
Uri.lean chore: avoid runtime array bounds checks (#6134) 2024-11-21 05:04:52 +00:00