lean4-htt/src/Init/System
Sebastian Ullrich b548b4faae
refactor: make Promise implementation opaque (#3273)
This follows the standard `Ref` recipe and moves the `unsafeCast` into
C++
2024-02-09 10:43:41 +00:00
..
FilePath.lean fix: do not strip dotted components from lean module names (#2994) 2024-01-10 14:24:26 +00:00
IO.lean feat: synchronous execution of task continuations (#3013) 2024-01-25 13:54:20 +00:00
IOError.lean feat: log2 for Fin and UInts 2022-11-29 01:05:06 +01:00
Mutex.lean chore: use deriving Nonempty 2022-12-22 03:48:15 +01:00
Platform.lean feat: System.Platform.target (#3207) 2024-01-24 12:11:00 +00:00
Promise.lean refactor: make Promise implementation opaque (#3273) 2024-02-09 10:43:41 +00:00
ST.lean feat: code action resolvers 2022-10-20 11:20:42 -07:00
Uri.lean chore: fix more typos in comments 2023-10-08 14:37:34 -07:00