diff --git a/library/init/lean/elaborator.lean b/library/init/lean/elaborator.lean index ffc3f0ff25..b859dbf582 100644 --- a/library/init/lean/elaborator.lean +++ b/library/init/lean/elaborator.lean @@ -392,7 +392,7 @@ def decl_modifiers_to_pexpr (mods : decl_modifiers.view) : elaborator_m expr := | some (visibility.view.protected _) := mdata.set_bool `protected tt | _ := mdata, let mdata := mdata.set_bool `noncomputable mods.noncomputable.is_some, - let mdata := mdata.set_bool `meta mods.meta.is_some, + let mdata := mdata.set_bool `unsafe mods.unsafe.is_some, expr.mdata mdata <$> attrs_to_pexpr (match mods.attrs with | some attrs := attrs.attrs | none := []) diff --git a/library/init/lean/parser/command.lean b/library/init/lean/parser/command.lean index 3d827a1c60..56f65de63f 100644 --- a/library/init/lean/parser/command.lean +++ b/library/init/lean/parser/command.lean @@ -117,7 +117,7 @@ def builtin_command_parsers : token_map command_parser := token_map.of_list [ ("private", declaration.parser), ("protected", declaration.parser), ("noncomputable", declaration.parser), - ("meta", declaration.parser), + ("unsafe", declaration.parser), ("def", declaration.parser), ("abbreviation", declaration.parser), ("theorem", declaration.parser), diff --git a/library/init/lean/parser/declaration.lean b/library/init/lean/parser/declaration.lean index d9bd13e8b0..1f5d06b020 100644 --- a/library/init/lean/parser/declaration.lean +++ b/library/init/lean/parser/declaration.lean @@ -46,7 +46,7 @@ node! decl_modifiers [ attrs: decl_attributes.parser?, visibility: node_choice! visibility {"private", "protected"}?, «noncomputable»: (symbol "noncomputable")?, - «meta»: (symbol "meta")?, + «unsafe»: (symbol "unsafe")?, ] @[derive has_tokens has_view] diff --git a/src/boot/init/io.cpp b/src/boot/init/io.cpp index 8b4ea3008e..bd4e7a86fc 100644 --- a/src/boot/init/io.cpp +++ b/src/boot/init/io.cpp @@ -111,14 +111,14 @@ obj* l_io_prim_iterate___at_io_fs_handle_read__to__end___spec__4___lambda__1(obj obj* l_io_fs_handle_get__line___rarg(obj*, obj*, obj*, obj*, obj*); obj* l_eio__unit_has__eval___rarg(obj*, obj*, obj*); obj* l_io_prim_iterate__aux(obj*, obj*); -extern "C" obj* lean_io_unsafe(obj*, obj*); +extern "C" obj* lean_io_unsafe(obj*, obj*, obj*); obj* l_io_fs_read__file(obj*, obj*); obj* l___private_init_io_13__put__str___at_io_println_x_27___spec__3___boxed(obj*, obj*); obj* l_io_prim_lift__eio___boxed(obj*, obj*, obj*); obj* l_io_fs_handle_flush___boxed(obj*, obj*); obj* l_state__t_pure___at_io_prim_io__inhabited___spec__1(obj*); extern "C" obj* lean_io_prim_handle_get_line(obj*, obj*); -obj* l_unsafe__io___boxed(obj*, obj*); +obj* l_unsafe__io___boxed(obj*, obj*, obj*); obj* l_io_lazy__pure(obj*); obj* l_io_fs_handle_mk(obj*, obj*); obj* l_io_fs_read__file___rarg___lambda__1___boxed(obj*, obj*, obj*); @@ -181,12 +181,12 @@ x_10 = l_state__t_monad___rarg(x_9); return x_10; } } -obj* l_unsafe__io___boxed(obj* x_0, obj* x_1) { +obj* l_unsafe__io___boxed(obj* x_0, obj* x_1, obj* x_2) { _start: { -obj* x_2; -x_2 = lean_io_unsafe(x_0, x_1); -return x_2; +obj* x_3; +x_3 = lean_io_unsafe(x_0, x_1, x_2); +return x_3; } } obj* l_timeit___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3) { diff --git a/src/boot/init/lean/elaborator.cpp b/src/boot/init/lean/elaborator.cpp index 2f37031710..edfe301328 100644 --- a/src/boot/init/lean/elaborator.cpp +++ b/src/boot/init/lean/elaborator.cpp @@ -17715,7 +17715,7 @@ _start: { obj* x_0; obj* x_1; obj* x_2; x_0 = lean::box(0); -x_1 = lean::mk_string("meta"); +x_1 = lean::mk_string("unsafe"); x_2 = lean_name_mk_string(x_0, x_1); return x_2; } diff --git a/src/boot/init/lean/parser/command.cpp b/src/boot/init/lean/parser/command.cpp index c549e8f3cb..64a97ca86d 100644 --- a/src/boot/init/lean/parser/command.cpp +++ b/src/boot/init/lean/parser/command.cpp @@ -13753,7 +13753,7 @@ lean::inc(x_3); x_21 = lean::alloc_cnstr(0, 2, 0); lean::cnstr_set(x_21, 0, x_19); lean::cnstr_set(x_21, 1, x_3); -x_22 = lean::mk_string("meta"); +x_22 = lean::mk_string("unsafe"); x_23 = lean_name_mk_string(x_0, x_22); lean::inc(x_3); x_25 = lean::alloc_cnstr(0, 2, 0); diff --git a/src/boot/init/lean/parser/declaration.cpp b/src/boot/init/lean/parser/declaration.cpp index 0a777da584..3068ec8f74 100644 --- a/src/boot/init/lean/parser/declaration.cpp +++ b/src/boot/init/lean/parser/declaration.cpp @@ -10421,7 +10421,7 @@ x_26 = l_lean_parser_symbol_tokens___rarg(x_25, x_5); lean::dec(x_25); x_28 = l_lean_parser_tokens___rarg(x_26); lean::dec(x_26); -x_30 = lean::mk_string("meta"); +x_30 = lean::mk_string("unsafe"); x_31 = l_lean_parser_symbol_tokens___rarg(x_30, x_5); lean::dec(x_30); x_33 = l_lean_parser_tokens___rarg(x_31); @@ -10507,7 +10507,7 @@ lean::closure_set(x_30, 1, x_9); lean::closure_set(x_30, 2, x_29); x_31 = lean::alloc_closure(reinterpret_cast(l_lean_parser_combinators_optional___at_lean_parser_command_decl__modifiers_parser_lean_parser_has__tokens___spec__1), 5, 1); lean::closure_set(x_31, 0, x_30); -x_32 = lean::mk_string("meta"); +x_32 = lean::mk_string("unsafe"); x_33 = l_string_trim(x_32); lean::dec(x_32); lean::inc(x_33); @@ -10607,7 +10607,7 @@ lean::closure_set(x_30, 1, x_9); lean::closure_set(x_30, 2, x_29); x_31 = lean::alloc_closure(reinterpret_cast(l_lean_parser_combinators_optional___at_lean_parser_command_decl__modifiers_parser_lean_parser_has__tokens___spec__1), 5, 1); lean::closure_set(x_31, 0, x_30); -x_32 = lean::mk_string("meta"); +x_32 = lean::mk_string("unsafe"); x_33 = l_string_trim(x_32); lean::dec(x_32); lean::inc(x_33);