diff --git a/script/gen_tokens_cpp.py b/script/gen_tokens_cpp.py index ea9492536..73dfd41d2 100644 --- a/script/gen_tokens_cpp.py +++ b/script/gen_tokens_cpp.py @@ -63,7 +63,7 @@ def main(argv=None): f.write('namespace lean{\n') # declare constants for c in constants: - f.write('name const * g_%s_tk = nullptr;\n' % c[0]) + f.write('static name const * g_%s_tk = nullptr;\n' % c[0]) # initialize constants f.write('void initialize_tokens() {\n') for c in constants: diff --git a/src/frontends/lean/tokens.cpp b/src/frontends/lean/tokens.cpp index 43e18e306..a59c78ada 100644 --- a/src/frontends/lean/tokens.cpp +++ b/src/frontends/lean/tokens.cpp @@ -3,138 +3,138 @@ // DO NOT EDIT, automatically generated file, generator scripts/gen_tokens_cpp.py #include "util/name.h" namespace lean{ -name const * g_period_tk = nullptr; -name const * g_placeholder_tk = nullptr; -name const * g_colon_tk = nullptr; -name const * g_semicolon_tk = nullptr; -name const * g_dcolon_tk = nullptr; -name const * g_lparen_tk = nullptr; -name const * g_rparen_tk = nullptr; -name const * g_llevel_curly_tk = nullptr; -name const * g_lcurly_tk = nullptr; -name const * g_rcurly_tk = nullptr; -name const * g_ldcurly_tk = nullptr; -name const * g_rdcurly_tk = nullptr; -name const * g_lcurlybar_tk = nullptr; -name const * g_rcurlybar_tk = nullptr; -name const * g_lbracket_tk = nullptr; -name const * g_rbracket_tk = nullptr; -name const * g_langle_tk = nullptr; -name const * g_rangle_tk = nullptr; -name const * g_triangle_tk = nullptr; -name const * g_caret_tk = nullptr; -name const * g_up_tk = nullptr; -name const * g_down_tk = nullptr; -name const * g_bar_tk = nullptr; -name const * g_comma_tk = nullptr; -name const * g_add_tk = nullptr; -name const * g_sub_tk = nullptr; -name const * g_greater_tk = nullptr; -name const * g_question_tk = nullptr; -name const * g_question_lp_tk = nullptr; -name const * g_bang_tk = nullptr; -name const * g_slash_tk = nullptr; -name const * g_plus_tk = nullptr; -name const * g_star_tk = nullptr; -name const * g_turnstile_tk = nullptr; -name const * g_explicit_tk = nullptr; -name const * g_max_tk = nullptr; -name const * g_imax_tk = nullptr; -name const * g_cup_tk = nullptr; -name const * g_import_tk = nullptr; -name const * g_prelude_tk = nullptr; -name const * g_show_tk = nullptr; -name const * g_have_tk = nullptr; -name const * g_assert_tk = nullptr; -name const * g_assume_tk = nullptr; -name const * g_take_tk = nullptr; -name const * g_fun_tk = nullptr; -name const * g_match_tk = nullptr; -name const * g_ellipsis_tk = nullptr; -name const * g_raw_tk = nullptr; -name const * g_true_tk = nullptr; -name const * g_false_tk = nullptr; -name const * g_options_tk = nullptr; -name const * g_commands_tk = nullptr; -name const * g_instances_tk = nullptr; -name const * g_classes_tk = nullptr; -name const * g_coercions_tk = nullptr; -name const * g_arrow_tk = nullptr; -name const * g_declarations_tk = nullptr; -name const * g_decls_tk = nullptr; -name const * g_hiding_tk = nullptr; -name const * g_exposing_tk = nullptr; -name const * g_renaming_tk = nullptr; -name const * g_replacing_tk = nullptr; -name const * g_extends_tk = nullptr; -name const * g_as_tk = nullptr; -name const * g_none_tk = nullptr; -name const * g_whnf_tk = nullptr; -name const * g_wf_tk = nullptr; -name const * g_in_tk = nullptr; -name const * g_at_tk = nullptr; -name const * g_assign_tk = nullptr; -name const * g_visible_tk = nullptr; -name const * g_from_tk = nullptr; -name const * g_using_tk = nullptr; -name const * g_then_tk = nullptr; -name const * g_else_tk = nullptr; -name const * g_by_tk = nullptr; -name const * g_rewrite_tk = nullptr; -name const * g_proof_tk = nullptr; -name const * g_qed_tk = nullptr; -name const * g_begin_tk = nullptr; -name const * g_begin_plus_tk = nullptr; -name const * g_end_tk = nullptr; -name const * g_private_tk = nullptr; -name const * g_definition_tk = nullptr; -name const * g_theorem_tk = nullptr; -name const * g_abbreviation_tk = nullptr; -name const * g_axiom_tk = nullptr; -name const * g_axioms_tk = nullptr; -name const * g_constant_tk = nullptr; -name const * g_constants_tk = nullptr; -name const * g_variable_tk = nullptr; -name const * g_variables_tk = nullptr; -name const * g_instance_tk = nullptr; -name const * g_priority_tk = nullptr; -name const * g_unfold_c_tk = nullptr; -name const * g_unfold_f_tk = nullptr; -name const * g_constructor_tk = nullptr; -name const * g_coercion_tk = nullptr; -name const * g_reducible_tk = nullptr; -name const * g_quasireducible_tk = nullptr; -name const * g_semireducible_tk = nullptr; -name const * g_irreducible_tk = nullptr; -name const * g_parsing_only_tk = nullptr; -name const * g_symm_tk = nullptr; -name const * g_trans_tk = nullptr; -name const * g_refl_tk = nullptr; -name const * g_subst_tk = nullptr; -name const * g_recursor_tk = nullptr; -name const * g_attribute_tk = nullptr; -name const * g_with_tk = nullptr; -name const * g_class_tk = nullptr; -name const * g_multiple_instances_tk = nullptr; -name const * g_prev_tk = nullptr; -name const * g_scoped_tk = nullptr; -name const * g_foldr_tk = nullptr; -name const * g_foldl_tk = nullptr; -name const * g_binder_tk = nullptr; -name const * g_binders_tk = nullptr; -name const * g_infix_tk = nullptr; -name const * g_infixl_tk = nullptr; -name const * g_infixr_tk = nullptr; -name const * g_postfix_tk = nullptr; -name const * g_prefix_tk = nullptr; -name const * g_notation_tk = nullptr; -name const * g_call_tk = nullptr; -name const * g_persistent_tk = nullptr; -name const * g_root_tk = nullptr; -name const * g_fields_tk = nullptr; -name const * g_trust_tk = nullptr; -name const * g_metaclasses_tk = nullptr; -name const * g_inductive_tk = nullptr; +static name const * g_period_tk = nullptr; +static name const * g_placeholder_tk = nullptr; +static name const * g_colon_tk = nullptr; +static name const * g_semicolon_tk = nullptr; +static name const * g_dcolon_tk = nullptr; +static name const * g_lparen_tk = nullptr; +static name const * g_rparen_tk = nullptr; +static name const * g_llevel_curly_tk = nullptr; +static name const * g_lcurly_tk = nullptr; +static name const * g_rcurly_tk = nullptr; +static name const * g_ldcurly_tk = nullptr; +static name const * g_rdcurly_tk = nullptr; +static name const * g_lcurlybar_tk = nullptr; +static name const * g_rcurlybar_tk = nullptr; +static name const * g_lbracket_tk = nullptr; +static name const * g_rbracket_tk = nullptr; +static name const * g_langle_tk = nullptr; +static name const * g_rangle_tk = nullptr; +static name const * g_triangle_tk = nullptr; +static name const * g_caret_tk = nullptr; +static name const * g_up_tk = nullptr; +static name const * g_down_tk = nullptr; +static name const * g_bar_tk = nullptr; +static name const * g_comma_tk = nullptr; +static name const * g_add_tk = nullptr; +static name const * g_sub_tk = nullptr; +static name const * g_greater_tk = nullptr; +static name const * g_question_tk = nullptr; +static name const * g_question_lp_tk = nullptr; +static name const * g_bang_tk = nullptr; +static name const * g_slash_tk = nullptr; +static name const * g_plus_tk = nullptr; +static name const * g_star_tk = nullptr; +static name const * g_turnstile_tk = nullptr; +static name const * g_explicit_tk = nullptr; +static name const * g_max_tk = nullptr; +static name const * g_imax_tk = nullptr; +static name const * g_cup_tk = nullptr; +static name const * g_import_tk = nullptr; +static name const * g_prelude_tk = nullptr; +static name const * g_show_tk = nullptr; +static name const * g_have_tk = nullptr; +static name const * g_assert_tk = nullptr; +static name const * g_assume_tk = nullptr; +static name const * g_take_tk = nullptr; +static name const * g_fun_tk = nullptr; +static name const * g_match_tk = nullptr; +static name const * g_ellipsis_tk = nullptr; +static name const * g_raw_tk = nullptr; +static name const * g_true_tk = nullptr; +static name const * g_false_tk = nullptr; +static name const * g_options_tk = nullptr; +static name const * g_commands_tk = nullptr; +static name const * g_instances_tk = nullptr; +static name const * g_classes_tk = nullptr; +static name const * g_coercions_tk = nullptr; +static name const * g_arrow_tk = nullptr; +static name const * g_declarations_tk = nullptr; +static name const * g_decls_tk = nullptr; +static name const * g_hiding_tk = nullptr; +static name const * g_exposing_tk = nullptr; +static name const * g_renaming_tk = nullptr; +static name const * g_replacing_tk = nullptr; +static name const * g_extends_tk = nullptr; +static name const * g_as_tk = nullptr; +static name const * g_none_tk = nullptr; +static name const * g_whnf_tk = nullptr; +static name const * g_wf_tk = nullptr; +static name const * g_in_tk = nullptr; +static name const * g_at_tk = nullptr; +static name const * g_assign_tk = nullptr; +static name const * g_visible_tk = nullptr; +static name const * g_from_tk = nullptr; +static name const * g_using_tk = nullptr; +static name const * g_then_tk = nullptr; +static name const * g_else_tk = nullptr; +static name const * g_by_tk = nullptr; +static name const * g_rewrite_tk = nullptr; +static name const * g_proof_tk = nullptr; +static name const * g_qed_tk = nullptr; +static name const * g_begin_tk = nullptr; +static name const * g_begin_plus_tk = nullptr; +static name const * g_end_tk = nullptr; +static name const * g_private_tk = nullptr; +static name const * g_definition_tk = nullptr; +static name const * g_theorem_tk = nullptr; +static name const * g_abbreviation_tk = nullptr; +static name const * g_axiom_tk = nullptr; +static name const * g_axioms_tk = nullptr; +static name const * g_constant_tk = nullptr; +static name const * g_constants_tk = nullptr; +static name const * g_variable_tk = nullptr; +static name const * g_variables_tk = nullptr; +static name const * g_instance_tk = nullptr; +static name const * g_priority_tk = nullptr; +static name const * g_unfold_c_tk = nullptr; +static name const * g_unfold_f_tk = nullptr; +static name const * g_constructor_tk = nullptr; +static name const * g_coercion_tk = nullptr; +static name const * g_reducible_tk = nullptr; +static name const * g_quasireducible_tk = nullptr; +static name const * g_semireducible_tk = nullptr; +static name const * g_irreducible_tk = nullptr; +static name const * g_parsing_only_tk = nullptr; +static name const * g_symm_tk = nullptr; +static name const * g_trans_tk = nullptr; +static name const * g_refl_tk = nullptr; +static name const * g_subst_tk = nullptr; +static name const * g_recursor_tk = nullptr; +static name const * g_attribute_tk = nullptr; +static name const * g_with_tk = nullptr; +static name const * g_class_tk = nullptr; +static name const * g_multiple_instances_tk = nullptr; +static name const * g_prev_tk = nullptr; +static name const * g_scoped_tk = nullptr; +static name const * g_foldr_tk = nullptr; +static name const * g_foldl_tk = nullptr; +static name const * g_binder_tk = nullptr; +static name const * g_binders_tk = nullptr; +static name const * g_infix_tk = nullptr; +static name const * g_infixl_tk = nullptr; +static name const * g_infixr_tk = nullptr; +static name const * g_postfix_tk = nullptr; +static name const * g_prefix_tk = nullptr; +static name const * g_notation_tk = nullptr; +static name const * g_call_tk = nullptr; +static name const * g_persistent_tk = nullptr; +static name const * g_root_tk = nullptr; +static name const * g_fields_tk = nullptr; +static name const * g_trust_tk = nullptr; +static name const * g_metaclasses_tk = nullptr; +static name const * g_inductive_tk = nullptr; void initialize_tokens() { g_period_tk = new name{"."}; g_placeholder_tk = new name{"_"};