lean4-htt/src/Init/System
euprunin 88078930a9
chore: fix spelling mistakes (#8324)
Co-authored-by: euprunin <euprunin@users.noreply.github.com>
2025-05-14 06:52:16 +00:00
..
FilePath.lean chore: do not use the coercion α → Option α in Init and Std (#8085) 2025-04-24 13:35:01 +00:00
IO.lean chore: fix spelling mistakes (#8324) 2025-05-14 06:52:16 +00:00
IOError.lean chore: do not use the coercion α → Option α in Init and Std (#8085) 2025-04-24 13:35:01 +00:00
Mutex.lean feat: enable experimental module system in Init (#8047) 2025-04-23 17:21:33 +00:00
Platform.lean feat: enable experimental module system in Init (#8047) 2025-04-23 17:21:33 +00:00
Promise.lean feat: enable experimental module system in Init (#8047) 2025-04-23 17:21:33 +00:00
ST.lean feat: enable experimental module system in Init (#8047) 2025-04-23 17:21:33 +00:00
Uri.lean feat: enable experimental module system in Init (#8047) 2025-04-23 17:21:33 +00:00