|
include/lean
|
feat: new String.Slice API (#10514)
|
2025-09-25 12:18:52 +00:00 |
|
Init
|
chore: String.getUTF8Byte (#10637)
|
2025-10-01 13:59:42 +00:00 |
|
kernel
|
chore: turn some crashes into errors (#8402)
|
2025-09-24 13:04:18 +00:00 |
|
lake
|
chore: rename String.Pos to String.Pos.Raw (#10624)
|
2025-10-01 07:45:24 +00:00 |
|
Lean
|
fix: hygiene for goals generated by mvcgen (#10639)
|
2025-10-01 14:13:15 +00:00 |
|
runtime
|
feat: new String.Slice API (#10514)
|
2025-09-25 12:18:52 +00:00 |
|
Std
|
chore: rename String.Pos to String.Pos.Raw (#10624)
|
2025-10-01 07:45:24 +00:00 |
|
Init.lean
|
feat: overhaul meta system (#10362)
|
2025-09-17 21:04:29 +00:00 |