It looks like these aren't currently implemented? See https://web.archive.org/web/20250619083120/https://lean-lang.org/blog/2024-2-4-lean-450/