diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 689f5c295e..71dbe89503 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -21,6 +21,7 @@ Author: Leonardo de Moura
 #include "library/aux_recursors.h"
 #include "library/app_builder.h"
 #include "library/constants.h"
+#include "library/suffixes.h"
 #include "library/placeholder.h"
 #include "library/explicit.h"
 #include "library/string.h"
@@ -398,7 +399,7 @@ auto elaborator::get_elim_info_for_builtin(name const & fn) -> elim_info {
     nminors              = length(I_val.get_cnstrs());
 
     elim_info r;
-    if (fn.get_string() == "brec_on" || fn.get_string() == "binduction_on") {
+    if (fn.get_string() == g_brec_on || fn.get_string() == g_binduction_on) {
         r.m_arity      = nparams + 1 /* motive */ + nindices + 1 /* major */ + 1;
     } else {
         r.m_arity      = nparams + 1 /* motive */ + nindices + 1 /* major */ + nminors;
diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp
index 4b77362270..3189832095 100644
--- a/src/frontends/lean/structure_cmd.cpp
+++ b/src/frontends/lean/structure_cmd.cpp
@@ -37,6 +37,7 @@ Author: Leonardo de Moura
 #include "library/aux_recursors.h"
 #include "library/type_context.h"
 #include "library/app_builder.h"
+#include "library/suffixes.h"
 #include "library/compiler/compiler.h"
 #include "library/constructions/rec_on.h"
 #include "library/constructions/projection.h"
@@ -1149,7 +1150,7 @@ struct structure_cmd_fn {
     }
 
     void add_rec_on_alias(name const & n) {
-        name rec_on_name(m_name, "rec_on");
+        name rec_on_name(m_name, g_rec_on);
         constant_info rec_on_decl = m_env.get(rec_on_name);
         declaration new_decl = mk_definition_inferring_unsafe(m_env, n, rec_on_decl.get_lparams(),
                                                               rec_on_decl.get_type(), rec_on_decl.get_value(),
@@ -1161,10 +1162,10 @@ struct structure_cmd_fn {
 
     void declare_auxiliary() {
         m_env = mk_rec_on(m_env, m_name);
-        name rec_on_name(m_name, "rec_on");
+        name rec_on_name(m_name, g_rec_on);
         add_rec_alias(rec_on_name);
         m_env = add_aux_recursor(m_env, rec_on_name);
-        name cases_on_name(m_name, "cases_on");
+        name cases_on_name(m_name, g_cases_on);
         add_rec_on_alias(cases_on_name);
         m_env = add_aux_recursor(m_env, cases_on_name);
     }
@@ -1264,7 +1265,7 @@ struct structure_cmd_fn {
         if (!has_heq_decls(m_env))
             return;
         m_env = mk_no_confusion(m_env, m_name);
-        name no_confusion_name(m_name, "no_confusion");
+        name no_confusion_name(m_name, g_no_confusion);
         add_alias(no_confusion_name);
     }
 
diff --git a/src/library/compiler/llnf.cpp b/src/library/compiler/llnf.cpp
index 18815dba63..243e58b97f 100644
--- a/src/library/compiler/llnf.cpp
+++ b/src/library/compiler/llnf.cpp
@@ -581,7 +581,7 @@ class to_lambda_pure_fn {
         expr reachable_case;
         unsigned num_reachable = 0;
         expr some_reachable;
-        /* We use `is_id` to track whether this "cases_on"-application is of the form
+        /* We use `is_id` to track whether this "g_cases_on"-application is of the form
            ```
            C.cases_on major (fun ..., _cnstr.0.0) ... (fun ..., _cnstr.(n-1).0)
            ```
@@ -638,7 +638,7 @@ class to_lambda_pure_fn {
                 minor      = ensure_terminal(minor);
             minor          = visit(minor);
             if (!is_enf_unreachable(minor)) {
-                /* If `minor` is not the constructor `i`, then this "cases_on" application is not the identity. */
+                /* If `minor` is not the constructor `i`, then this "g_cases_on" application is not the identity. */
                 unsigned cidx, nusizes, ssz;
                 if (!(is_llnf_cnstr(minor, cidx, nusizes, ssz) && cidx == i && nusizes == 0 && ssz == 0)) {
                     is_id = false;
diff --git a/src/library/compiler/util.cpp b/src/library/compiler/util.cpp
index d9df5e4d50..3ed32d3b05 100644
--- a/src/library/compiler/util.cpp
+++ b/src/library/compiler/util.cpp
@@ -16,6 +16,7 @@ Author: Leonardo de Moura
 #include "kernel/instantiate.h"
 #include "kernel/kernel_exception.h"
 #include "library/util.h"
+#include "library/suffixes.h"
 #include "library/attribute_manager.h"
 #include "library/aux_recursors.h"
 #include "library/replace_visitor.h"
@@ -196,7 +197,7 @@ expr unfold_macro_defs(environment const & env, expr const & e) {
 }
 
 bool is_cases_on_recursor(environment const & env, name const & n) {
-    return ::lean::is_aux_recursor(env, n) && n.get_string() == "cases_on";
+    return ::lean::is_aux_recursor(env, n) && n.get_string() == g_cases_on;
 }
 
 unsigned get_cases_on_arity(environment const & env, name const & c, bool before_erasure) {
diff --git a/src/library/constants.cpp b/src/library/constants.cpp
index 62ff5f280d..5c6b444c32 100644
--- a/src/library/constants.cpp
+++ b/src/library/constants.cpp
@@ -22,15 +22,15 @@ name const * g_bin_tree_node = nullptr;
 name const * g_bool = nullptr;
 name const * g_bool_ff = nullptr;
 name const * g_bool_tt = nullptr;
-name const * g_combinator_K = nullptr;
+name const * g_combinator_k = nullptr;
 name const * g_cast = nullptr;
 name const * g_char = nullptr;
 name const * g_char_mk = nullptr;
 name const * g_char_ne_of_vne = nullptr;
 name const * g_char_of_nat = nullptr;
 name const * g_char_of_nat_ne_of_ne = nullptr;
-name const * g_is_valid_char_range_1 = nullptr;
-name const * g_is_valid_char_range_2 = nullptr;
+name const * g_is_valid_char_range1 = nullptr;
+name const * g_is_valid_char_range2 = nullptr;
 name const * g_coe = nullptr;
 name const * g_coe_fn = nullptr;
 name const * g_coe_sort = nullptr;
@@ -45,7 +45,7 @@ name const * g_decidable_is_true = nullptr;
 name const * g_decidable_is_false = nullptr;
 name const * g_dite = nullptr;
 name const * g_empty = nullptr;
-name const * g_Exists = nullptr;
+name const * g_exists = nullptr;
 name const * g_eq = nullptr;
 name const * g_eq_cases_on = nullptr;
 name const * g_eq_rec_on = nullptr;
@@ -288,288 +288,288 @@ name const * g_well_founded_tactics_dec_tac = nullptr;
 name const * g_wf_term_hack = nullptr;
 void initialize_constants() {
     g_absurd = new name{"absurd"};
-    g_acc_cases_on = new name{"acc", "cases_on"};
-    g_acc_rec = new name{"acc", "rec"};
+    g_acc_cases_on = new name{"Acc", "casesOn"};
+    g_acc_rec = new name{"Acc", "rec"};
     g_and = new name{"and"};
-    g_and_elim_left = new name{"and", "elim_left"};
-    g_and_elim_right = new name{"and", "elim_right"};
+    g_and_elim_left = new name{"and", "elimLeft"};
+    g_and_elim_right = new name{"and", "elimRight"};
     g_and_intro = new name{"and", "intro"};
     g_and_rec = new name{"and", "rec"};
-    g_and_cases_on = new name{"and", "cases_on"};
-    g_array = new name{"array"};
-    g_auto_param = new name{"auto_param"};
+    g_and_cases_on = new name{"and", "casesOn"};
+    g_array = new name{"Array"};
+    g_auto_param = new name{"autoParam"};
     g_bit0 = new name{"bit0"};
     g_bit1 = new name{"bit1"};
-    g_bin_tree_empty = new name{"bin_tree", "empty"};
-    g_bin_tree_leaf = new name{"bin_tree", "leaf"};
-    g_bin_tree_node = new name{"bin_tree", "node"};
-    g_bool = new name{"bool"};
-    g_bool_ff = new name{"bool", "ff"};
-    g_bool_tt = new name{"bool", "tt"};
-    g_combinator_K = new name{"combinator", "K"};
+    g_bin_tree_empty = new name{"BinTree", "Empty"};
+    g_bin_tree_leaf = new name{"BinTree", "leaf"};
+    g_bin_tree_node = new name{"BinTree", "Node"};
+    g_bool = new name{"Bool"};
+    g_bool_ff = new name{"Bool", "ff"};
+    g_bool_tt = new name{"Bool", "tt"};
+    g_combinator_k = new name{"Combinator", "K"};
     g_cast = new name{"cast"};
-    g_char = new name{"char"};
-    g_char_mk = new name{"char", "mk"};
-    g_char_ne_of_vne = new name{"char", "ne_of_vne"};
-    g_char_of_nat = new name{"char", "of_nat"};
-    g_char_of_nat_ne_of_ne = new name{"char", "of_nat_ne_of_ne"};
-    g_is_valid_char_range_1 = new name{"is_valid_char_range_1"};
-    g_is_valid_char_range_2 = new name{"is_valid_char_range_2"};
+    g_char = new name{"Char"};
+    g_char_mk = new name{"Char", "mk"};
+    g_char_ne_of_vne = new name{"Char", "neOfVne"};
+    g_char_of_nat = new name{"Char", "ofNat"};
+    g_char_of_nat_ne_of_ne = new name{"Char", "ofNatNeOfNe"};
+    g_is_valid_char_range1 = new name{"isValidCharRange1"};
+    g_is_valid_char_range2 = new name{"isValidCharRange2"};
     g_coe = new name{"coe"};
-    g_coe_fn = new name{"coe_fn"};
-    g_coe_sort = new name{"coe_sort"};
-    g_coe_to_lift = new name{"coe_to_lift"};
+    g_coe_fn = new name{"coeFn"};
+    g_coe_sort = new name{"coeSort"};
+    g_coe_to_lift = new name{"coeToLift"};
     g_congr = new name{"congr"};
-    g_congr_arg = new name{"congr_arg"};
-    g_congr_fun = new name{"congr_fun"};
-    g_decidable = new name{"decidable"};
-    g_decidable_cases_on = new name{"decidable", "cases_on"};
-    g_decidable_to_bool = new name{"decidable", "to_bool"};
-    g_decidable_is_true = new name{"decidable", "is_true"};
-    g_decidable_is_false = new name{"decidable", "is_false"};
+    g_congr_arg = new name{"congrArg"};
+    g_congr_fun = new name{"congrFun"};
+    g_decidable = new name{"Decidable"};
+    g_decidable_cases_on = new name{"Decidable", "casesOn"};
+    g_decidable_to_bool = new name{"Decidable", "toBool"};
+    g_decidable_is_true = new name{"Decidable", "isTrue"};
+    g_decidable_is_false = new name{"Decidable", "isFalse"};
     g_dite = new name{"dite"};
-    g_empty = new name{"empty"};
-    g_Exists = new name{"Exists"};
-    g_eq = new name{"eq"};
-    g_eq_cases_on = new name{"eq", "cases_on"};
-    g_eq_rec_on = new name{"eq", "rec_on"};
-    g_eq_rec = new name{"eq", "rec"};
-    g_eq_mp = new name{"eq", "mp"};
-    g_eq_mpr = new name{"eq", "mpr"};
-    g_eq_ndrec = new name{"eq", "ndrec"};
-    g_eq_refl = new name{"eq", "refl"};
-    g_eq_subst = new name{"eq", "subst"};
-    g_eq_symm = new name{"eq", "symm"};
-    g_eq_trans = new name{"eq", "trans"};
-    g_eq_of_heq = new name{"eq_of_heq"};
-    g_eq_true_intro = new name{"eq_true_intro"};
-    g_eq_false_intro = new name{"eq_false_intro"};
-    g_eq_self_iff_true = new name{"eq_self_iff_true"};
-    g_lean_level = new name{"lean", "level"};
-    g_lean_expr = new name{"lean", "expr"};
-    g_lean_expr_subst = new name{"lean", "expr", "subst"};
-    g_false = new name{"false"};
-    g_false_of_true_iff_false = new name{"false_of_true_iff_false"};
-    g_false_of_true_eq_false = new name{"false_of_true_eq_false"};
-    g_false_rec = new name{"false", "rec"};
-    g_false_cases_on = new name{"false", "cases_on"};
-    g_fin_mk = new name{"fin", "mk"};
-    g_fin_ne_of_vne = new name{"fin", "ne_of_vne"};
-    g_forall_congr = new name{"forall_congr"};
-    g_forall_congr_eq = new name{"forall_congr_eq"};
+    g_empty = new name{"Empty"};
+    g_exists = new name{"Exists"};
+    g_eq = new name{"Eq"};
+    g_eq_cases_on = new name{"Eq", "casesOn"};
+    g_eq_rec_on = new name{"Eq", "recOn"};
+    g_eq_rec = new name{"Eq", "rec"};
+    g_eq_mp = new name{"Eq", "mp"};
+    g_eq_mpr = new name{"Eq", "mpr"};
+    g_eq_ndrec = new name{"Eq", "ndrec"};
+    g_eq_refl = new name{"Eq", "refl"};
+    g_eq_subst = new name{"Eq", "subst"};
+    g_eq_symm = new name{"Eq", "symm"};
+    g_eq_trans = new name{"Eq", "trans"};
+    g_eq_of_heq = new name{"eqOfHeq"};
+    g_eq_true_intro = new name{"eqTrueIntro"};
+    g_eq_false_intro = new name{"eqFalseIntro"};
+    g_eq_self_iff_true = new name{"eqSelfIffTrue"};
+    g_lean_level = new name{"Lean", "Level"};
+    g_lean_expr = new name{"Lean", "Expr"};
+    g_lean_expr_subst = new name{"Lean", "Expr", "subst"};
+    g_false = new name{"False"};
+    g_false_of_true_iff_false = new name{"falseOfTrueIffFalse"};
+    g_false_of_true_eq_false = new name{"falseOfTrueEqFalse"};
+    g_false_rec = new name{"False", "rec"};
+    g_false_cases_on = new name{"False", "casesOn"};
+    g_fin_mk = new name{"Fin", "mk"};
+    g_fin_ne_of_vne = new name{"Fin", "neOfVne"};
+    g_forall_congr = new name{"forallCongr"};
+    g_forall_congr_eq = new name{"forallCongrEq"};
     g_funext = new name{"funext"};
-    g_has_add = new name{"has_add"};
-    g_has_add_add = new name{"has_add", "add"};
-    g_has_andthen_andthen = new name{"has_andthen", "andthen"};
-    g_has_bind_and_then = new name{"has_bind", "and_then"};
-    g_has_bind_seq = new name{"has_bind", "seq"};
-    g_has_div_div = new name{"has_div", "div"};
-    g_has_emptyc_emptyc = new name{"has_emptyc", "emptyc"};
-    g_has_eval = new name{"has_eval"};
-    g_has_eval_eval = new name{"has_eval", "eval"};
-    g_has_insert_insert = new name{"has_insert", "insert"};
-    g_has_neg_neg = new name{"has_neg", "neg"};
-    g_has_one = new name{"has_one"};
-    g_has_one_one = new name{"has_one", "one"};
-    g_has_orelse_orelse = new name{"has_orelse", "orelse"};
-    g_has_sep_sep = new name{"has_sep", "sep"};
-    g_has_sizeof = new name{"has_sizeof"};
-    g_has_sizeof_mk = new name{"has_sizeof", "mk"};
-    g_has_sub_sub = new name{"has_sub", "sub"};
-    g_has_repr = new name{"has_repr"};
-    g_has_well_founded = new name{"has_well_founded"};
-    g_has_well_founded_r = new name{"has_well_founded", "r"};
-    g_has_well_founded_wf = new name{"has_well_founded", "wf"};
-    g_has_zero = new name{"has_zero"};
-    g_has_zero_zero = new name{"has_zero", "zero"};
-    g_has_coe_t = new name{"has_coe_t"};
-    g_heq = new name{"heq"};
-    g_heq_refl = new name{"heq", "refl"};
-    g_heq_symm = new name{"heq", "symm"};
-    g_heq_trans = new name{"heq", "trans"};
-    g_heq_of_eq = new name{"heq_of_eq"};
+    g_has_add = new name{"HasAdd"};
+    g_has_add_add = new name{"HasAdd", "add"};
+    g_has_andthen_andthen = new name{"HasAndthen", "andthen"};
+    g_has_bind_and_then = new name{"HasBind", "andThen"};
+    g_has_bind_seq = new name{"HasBind", "Seq"};
+    g_has_div_div = new name{"HasDiv", "div"};
+    g_has_emptyc_emptyc = new name{"HasEmptyc", "emptyc"};
+    g_has_eval = new name{"HasEval"};
+    g_has_eval_eval = new name{"HasEval", "eval"};
+    g_has_insert_insert = new name{"HasInsert", "insert"};
+    g_has_neg_neg = new name{"HasNeg", "neg"};
+    g_has_one = new name{"HasOne"};
+    g_has_one_one = new name{"HasOne", "one"};
+    g_has_orelse_orelse = new name{"HasOrelse", "orelse"};
+    g_has_sep_sep = new name{"HasSep", "sep"};
+    g_has_sizeof = new name{"HasSizeof"};
+    g_has_sizeof_mk = new name{"HasSizeof", "mk"};
+    g_has_sub_sub = new name{"HasSub", "sub"};
+    g_has_repr = new name{"HasRepr"};
+    g_has_well_founded = new name{"HasWellFounded"};
+    g_has_well_founded_r = new name{"HasWellFounded", "r"};
+    g_has_well_founded_wf = new name{"HasWellFounded", "wf"};
+    g_has_zero = new name{"HasZero"};
+    g_has_zero_zero = new name{"HasZero", "zero"};
+    g_has_coe_t = new name{"HasCoeT"};
+    g_heq = new name{"Heq"};
+    g_heq_refl = new name{"Heq", "refl"};
+    g_heq_symm = new name{"Heq", "symm"};
+    g_heq_trans = new name{"Heq", "trans"};
+    g_heq_of_eq = new name{"heqOfEq"};
     g_id = new name{"id"};
-    g_id_rhs = new name{"id_rhs"};
-    g_id_delta = new name{"id_delta"};
-    g_if_neg = new name{"if_neg"};
-    g_if_pos = new name{"if_pos"};
-    g_iff = new name{"iff"};
-    g_iff_false_intro = new name{"iff_false_intro"};
-    g_iff_intro = new name{"iff", "intro"};
-    g_iff_mp = new name{"iff", "mp"};
-    g_iff_mpr = new name{"iff", "mpr"};
-    g_iff_refl = new name{"iff", "refl"};
-    g_iff_symm = new name{"iff", "symm"};
-    g_iff_trans = new name{"iff", "trans"};
-    g_iff_true_intro = new name{"iff_true_intro"};
-    g_imp_congr = new name{"imp_congr"};
-    g_imp_congr_eq = new name{"imp_congr_eq"};
-    g_imp_congr_ctx = new name{"imp_congr_ctx"};
-    g_imp_congr_ctx_eq = new name{"imp_congr_ctx_eq"};
+    g_id_rhs = new name{"idRhs"};
+    g_id_delta = new name{"idDelta"};
+    g_if_neg = new name{"ifNeg"};
+    g_if_pos = new name{"ifPos"};
+    g_iff = new name{"Iff"};
+    g_iff_false_intro = new name{"iffFalseIntro"};
+    g_iff_intro = new name{"Iff", "intro"};
+    g_iff_mp = new name{"Iff", "mp"};
+    g_iff_mpr = new name{"Iff", "mpr"};
+    g_iff_refl = new name{"Iff", "refl"};
+    g_iff_symm = new name{"Iff", "symm"};
+    g_iff_trans = new name{"Iff", "trans"};
+    g_iff_true_intro = new name{"iffTrueIntro"};
+    g_imp_congr = new name{"impCongr"};
+    g_imp_congr_eq = new name{"impCongrEq"};
+    g_imp_congr_ctx = new name{"impCongrCtx"};
+    g_imp_congr_ctx_eq = new name{"impCongrCtxEq"};
     g_implies = new name{"implies"};
-    g_implies_of_if_neg = new name{"implies_of_if_neg"};
-    g_implies_of_if_pos = new name{"implies_of_if_pos"};
-    g_int = new name{"int"};
-    g_int_nat_abs = new name{"int", "nat_abs"};
-    g_int_lt = new name{"int", "lt"};
-    g_int_dec_lt = new name{"int", "dec_lt"};
-    g_int_of_nat = new name{"int", "of_nat"};
-    g_int_neg_succ_of_nat = new name{"int", "neg_succ_of_nat"};
-    g_interactive_param_desc = new name{"interactive", "param_desc"};
+    g_implies_of_if_neg = new name{"impliesOfIfNeg"};
+    g_implies_of_if_pos = new name{"impliesOfIfPos"};
+    g_int = new name{"Int"};
+    g_int_nat_abs = new name{"Int", "natAbs"};
+    g_int_lt = new name{"Int", "lt"};
+    g_int_dec_lt = new name{"Int", "decLt"};
+    g_int_of_nat = new name{"Int", "ofNat"};
+    g_int_neg_succ_of_nat = new name{"Int", "negSuccOfNat"};
+    g_interactive_param_desc = new name{"interactive", "paramDesc"};
     g_interactive_parse = new name{"interactive", "parse"};
-    g_io_core = new name{"io_core"};
-    g_monad_io_impl = new name{"monad_io_impl"};
-    g_monad_io_terminal_impl = new name{"monad_io_terminal_impl"};
-    g_monad_io_file_system_impl = new name{"monad_io_file_system_impl"};
-    g_monad_io_environment_impl = new name{"monad_io_environment_impl"};
-    g_monad_io_process_impl = new name{"monad_io_process_impl"};
-    g_monad_io_random_impl = new name{"monad_io_random_impl"};
+    g_io_core = new name{"ioCore"};
+    g_monad_io_impl = new name{"monadIoImpl"};
+    g_monad_io_terminal_impl = new name{"monadIoTerminalImpl"};
+    g_monad_io_file_system_impl = new name{"monadIoFileSystemImpl"};
+    g_monad_io_environment_impl = new name{"monadIoEnvironmentImpl"};
+    g_monad_io_process_impl = new name{"monadIoProcessImpl"};
+    g_monad_io_random_impl = new name{"monadIoRandomImpl"};
     g_inline = new name{"inline"};
-    g_io = new name{"io"};
+    g_io = new name{"Io"};
     g_ite = new name{"ite"};
-    g_lc_proof = new name{"lc_proof"};
-    g_lc_unreachable = new name{"lc_unreachable"};
-    g_list = new name{"list"};
-    g_list_nil = new name{"list", "nil"};
-    g_list_cons = new name{"list", "cons"};
-    g_match_failed = new name{"match_failed"};
-    g_monad = new name{"monad"};
-    g_monad_fail = new name{"monad_fail"};
-    g_lean_name = new name{"lean", "name"};
-    g_lean_name_anonymous = new name{"lean", "name", "anonymous"};
-    g_lean_name_mk_numeral = new name{"lean", "name", "mk_numeral"};
-    g_lean_name_mk_string = new name{"lean", "name", "mk_string"};
-    g_lean_name_no_confusion = new name{"lean", "name", "no_confusion"};
-    g_lean_name_mk_string_ne_mk_string_of_ne_prefix = new name{"lean", "name", "mk_string_ne_mk_string_of_ne_prefix"};
-    g_lean_name_mk_string_ne_mk_string_of_ne_string = new name{"lean", "name", "mk_string_ne_mk_string_of_ne_string"};
-    g_lean_name_mk_numeral_ne_mk_numeral_of_ne_prefix = new name{"lean", "name", "mk_numeral_ne_mk_numeral_of_ne_prefix"};
-    g_lean_name_mk_numeral_ne_mk_numeral_of_ne_numeral = new name{"lean", "name", "mk_numeral_ne_mk_numeral_of_ne_numeral"};
-    g_nat = new name{"nat"};
-    g_nat_succ = new name{"nat", "succ"};
-    g_nat_zero = new name{"nat", "zero"};
-    g_nat_has_zero = new name{"nat", "has_zero"};
-    g_nat_has_one = new name{"nat", "has_one"};
-    g_nat_has_add = new name{"nat", "has_add"};
-    g_nat_add = new name{"nat", "add"};
-    g_nat_cases_on = new name{"nat", "cases_on"};
-    g_nat_bit0_ne = new name{"nat", "bit0_ne"};
-    g_nat_bit0_ne_bit1 = new name{"nat", "bit0_ne_bit1"};
-    g_nat_bit0_ne_zero = new name{"nat", "bit0_ne_zero"};
-    g_nat_bit0_ne_one = new name{"nat", "bit0_ne_one"};
-    g_nat_bit1_ne = new name{"nat", "bit1_ne"};
-    g_nat_bit1_ne_bit0 = new name{"nat", "bit1_ne_bit0"};
-    g_nat_bit1_ne_zero = new name{"nat", "bit1_ne_zero"};
-    g_nat_bit1_ne_one = new name{"nat", "bit1_ne_one"};
-    g_nat_zero_ne_one = new name{"nat", "zero_ne_one"};
-    g_nat_zero_ne_bit0 = new name{"nat", "zero_ne_bit0"};
-    g_nat_zero_ne_bit1 = new name{"nat", "zero_ne_bit1"};
-    g_nat_one_ne_zero = new name{"nat", "one_ne_zero"};
-    g_nat_one_ne_bit0 = new name{"nat", "one_ne_bit0"};
-    g_nat_one_ne_bit1 = new name{"nat", "one_ne_bit1"};
-    g_nat_bit0_lt = new name{"nat", "bit0_lt"};
-    g_nat_bit1_lt = new name{"nat", "bit1_lt"};
-    g_nat_bit0_lt_bit1 = new name{"nat", "bit0_lt_bit1"};
-    g_nat_bit1_lt_bit0 = new name{"nat", "bit1_lt_bit0"};
-    g_nat_zero_lt_one = new name{"nat", "zero_lt_one"};
-    g_nat_zero_lt_bit1 = new name{"nat", "zero_lt_bit1"};
-    g_nat_zero_lt_bit0 = new name{"nat", "zero_lt_bit0"};
-    g_nat_one_lt_bit0 = new name{"nat", "one_lt_bit0"};
-    g_nat_one_lt_bit1 = new name{"nat", "one_lt_bit1"};
-    g_nat_le_of_lt = new name{"nat", "le_of_lt"};
-    g_nat_le_refl = new name{"nat", "le_refl"};
-    g_nat_decidable_lt = new name{"nat", "decidable_lt"};
-    g_nat_dec_eq = new name{"nat", "dec_eq"};
-    g_nat_mul = new name{"nat", "mul"};
-    g_nat_sub = new name{"nat", "sub"};
-    g_nat_beq = new name{"nat", "beq"};
-    g_nat_ble = new name{"nat", "ble"};
+    g_lc_proof = new name{"lcProof"};
+    g_lc_unreachable = new name{"lcUnreachable"};
+    g_list = new name{"List"};
+    g_list_nil = new name{"List", "nil"};
+    g_list_cons = new name{"List", "cons"};
+    g_match_failed = new name{"matchFailed"};
+    g_monad = new name{"Monad"};
+    g_monad_fail = new name{"MonadFail"};
+    g_lean_name = new name{"Lean", "Name"};
+    g_lean_name_anonymous = new name{"Lean", "Name", "anonymous"};
+    g_lean_name_mk_numeral = new name{"Lean", "Name", "mkNumeral"};
+    g_lean_name_mk_string = new name{"Lean", "Name", "mkString"};
+    g_lean_name_no_confusion = new name{"Lean", "Name", "noConfusion"};
+    g_lean_name_mk_string_ne_mk_string_of_ne_prefix = new name{"Lean", "Name", "mkStringNeMkStringOfNePrefix"};
+    g_lean_name_mk_string_ne_mk_string_of_ne_string = new name{"Lean", "Name", "mkStringNeMkStringOfNeString"};
+    g_lean_name_mk_numeral_ne_mk_numeral_of_ne_prefix = new name{"Lean", "Name", "mkNumeralNeMkNumeralOfNePrefix"};
+    g_lean_name_mk_numeral_ne_mk_numeral_of_ne_numeral = new name{"Lean", "Name", "mkNumeralNeMkNumeralOfNeNumeral"};
+    g_nat = new name{"Nat"};
+    g_nat_succ = new name{"Nat", "succ"};
+    g_nat_zero = new name{"Nat", "zero"};
+    g_nat_has_zero = new name{"Nat", "HasZero"};
+    g_nat_has_one = new name{"Nat", "HasOne"};
+    g_nat_has_add = new name{"Nat", "HasAdd"};
+    g_nat_add = new name{"Nat", "add"};
+    g_nat_cases_on = new name{"Nat", "casesOn"};
+    g_nat_bit0_ne = new name{"Nat", "bit0Ne"};
+    g_nat_bit0_ne_bit1 = new name{"Nat", "bit0NeBit1"};
+    g_nat_bit0_ne_zero = new name{"Nat", "bit0NeZero"};
+    g_nat_bit0_ne_one = new name{"Nat", "bit0NeOne"};
+    g_nat_bit1_ne = new name{"Nat", "bit1Ne"};
+    g_nat_bit1_ne_bit0 = new name{"Nat", "bit1NeBit0"};
+    g_nat_bit1_ne_zero = new name{"Nat", "bit1NeZero"};
+    g_nat_bit1_ne_one = new name{"Nat", "bit1NeOne"};
+    g_nat_zero_ne_one = new name{"Nat", "zeroNeOne"};
+    g_nat_zero_ne_bit0 = new name{"Nat", "zeroNeBit0"};
+    g_nat_zero_ne_bit1 = new name{"Nat", "zeroNeBit1"};
+    g_nat_one_ne_zero = new name{"Nat", "oneNeZero"};
+    g_nat_one_ne_bit0 = new name{"Nat", "oneNeBit0"};
+    g_nat_one_ne_bit1 = new name{"Nat", "oneNeBit1"};
+    g_nat_bit0_lt = new name{"Nat", "bit0Lt"};
+    g_nat_bit1_lt = new name{"Nat", "bit1Lt"};
+    g_nat_bit0_lt_bit1 = new name{"Nat", "bit0LtBit1"};
+    g_nat_bit1_lt_bit0 = new name{"Nat", "bit1LtBit0"};
+    g_nat_zero_lt_one = new name{"Nat", "zeroLtOne"};
+    g_nat_zero_lt_bit1 = new name{"Nat", "zeroLtBit1"};
+    g_nat_zero_lt_bit0 = new name{"Nat", "zeroLtBit0"};
+    g_nat_one_lt_bit0 = new name{"Nat", "oneLtBit0"};
+    g_nat_one_lt_bit1 = new name{"Nat", "oneLtBit1"};
+    g_nat_le_of_lt = new name{"Nat", "leOfLt"};
+    g_nat_le_refl = new name{"Nat", "leRefl"};
+    g_nat_decidable_lt = new name{"Nat", "decidableLt"};
+    g_nat_dec_eq = new name{"Nat", "decEq"};
+    g_nat_mul = new name{"Nat", "mul"};
+    g_nat_sub = new name{"Nat", "sub"};
+    g_nat_beq = new name{"Nat", "beq"};
+    g_nat_ble = new name{"Nat", "ble"};
     g_ne = new name{"ne"};
-    g_neq_of_not_iff = new name{"neq_of_not_iff"};
+    g_neq_of_not_iff = new name{"neqOfNotIff"};
     g_not = new name{"not"};
-    g_not_of_iff_false = new name{"not_of_iff_false"};
-    g_not_of_eq_false = new name{"not_of_eq_false"};
-    g_of_eq_true = new name{"of_eq_true"};
-    g_of_iff_true = new name{"of_iff_true"};
-    g_opt_param = new name{"opt_param"};
+    g_not_of_iff_false = new name{"notOfIffFalse"};
+    g_not_of_eq_false = new name{"notOfEqFalse"};
+    g_of_eq_true = new name{"ofEqTrue"};
+    g_of_iff_true = new name{"ofIffTrue"};
+    g_opt_param = new name{"optParam"};
     g_or = new name{"or"};
-    g_out_param = new name{"out_param"};
+    g_out_param = new name{"outParam"};
     g_pexpr = new name{"pexpr"};
     g_pexpr_subst = new name{"pexpr", "subst"};
-    g_punit = new name{"punit"};
-    g_punit_cases_on = new name{"punit", "cases_on"};
-    g_punit_star = new name{"punit", "star"};
-    g_prod_mk = new name{"prod", "mk"};
-    g_pprod = new name{"pprod"};
-    g_pprod_mk = new name{"pprod", "mk"};
-    g_pprod_fst = new name{"pprod", "fst"};
-    g_pprod_snd = new name{"pprod", "snd"};
+    g_punit = new name{"Punit"};
+    g_punit_cases_on = new name{"Punit", "casesOn"};
+    g_punit_star = new name{"Punit", "star"};
+    g_prod_mk = new name{"Prod", "mk"};
+    g_pprod = new name{"Pprod"};
+    g_pprod_mk = new name{"Pprod", "mk"};
+    g_pprod_fst = new name{"Pprod", "fst"};
+    g_pprod_snd = new name{"Pprod", "snd"};
     g_propext = new name{"propext"};
-    g_to_pexpr = new name{"to_pexpr"};
-    g_quot_mk = new name{"quot", "mk"};
-    g_quot_lift = new name{"quot", "lift"};
+    g_to_pexpr = new name{"toPexpr"};
+    g_quot_mk = new name{"Quot", "mk"};
+    g_quot_lift = new name{"Quot", "lift"};
     g_reflected = new name{"reflected"};
     g_reflected_subst = new name{"reflected", "subst"};
     g_repr = new name{"repr"};
     g_rfl = new name{"rfl"};
-    g_scope_trace = new name{"scope_trace"};
-    g_set_of = new name{"set_of"};
-    g_psigma = new name{"psigma"};
-    g_psigma_cases_on = new name{"psigma", "cases_on"};
-    g_psigma_mk = new name{"psigma", "mk"};
-    g_psigma_fst = new name{"psigma", "fst"};
-    g_psigma_snd = new name{"psigma", "snd"};
+    g_scope_trace = new name{"scopeTrace"};
+    g_set_of = new name{"setOf"};
+    g_psigma = new name{"Psigma"};
+    g_psigma_cases_on = new name{"Psigma", "casesOn"};
+    g_psigma_mk = new name{"Psigma", "mk"};
+    g_psigma_fst = new name{"Psigma", "fst"};
+    g_psigma_snd = new name{"Psigma", "snd"};
     g_singleton = new name{"singleton"};
     g_sizeof = new name{"sizeof"};
-    g_sorry_ax = new name{"sorry_ax"};
-    g_string = new name{"string"};
-    g_string_decidable_eq = new name{"string", "decidable_eq"};
-    g_string_mk = new name{"string", "mk"};
-    g_string_data = new name{"string", "data"};
-    g_string_empty = new name{"string", "empty"};
-    g_string_str = new name{"string", "str"};
-    g_string_empty_ne_str = new name{"string", "empty_ne_str"};
-    g_string_str_ne_empty = new name{"string", "str_ne_empty"};
-    g_string_str_ne_str_left = new name{"string", "str_ne_str_left"};
-    g_string_str_ne_str_right = new name{"string", "str_ne_str_right"};
+    g_sorry_ax = new name{"sorryAx"};
+    g_string = new name{"String"};
+    g_string_decidable_eq = new name{"String", "DecidableEq"};
+    g_string_mk = new name{"String", "mk"};
+    g_string_data = new name{"String", "data"};
+    g_string_empty = new name{"String", "Empty"};
+    g_string_str = new name{"String", "str"};
+    g_string_empty_ne_str = new name{"String", "emptyNeStr"};
+    g_string_str_ne_empty = new name{"String", "strNeEmpty"};
+    g_string_str_ne_str_left = new name{"String", "strNeStrLeft"};
+    g_string_str_ne_str_right = new name{"String", "strNeStrRight"};
     g_subsingleton = new name{"subsingleton"};
     g_subsingleton_elim = new name{"subsingleton", "elim"};
-    g_subtype = new name{"subtype"};
-    g_subtype_mk = new name{"subtype", "mk"};
-    g_subtype_val = new name{"subtype", "val"};
-    g_subtype_rec = new name{"subtype", "rec"};
-    g_psum = new name{"psum"};
-    g_psum_cases_on = new name{"psum", "cases_on"};
-    g_psum_inl = new name{"psum", "inl"};
-    g_psum_inr = new name{"psum", "inr"};
+    g_subtype = new name{"Subtype"};
+    g_subtype_mk = new name{"Subtype", "mk"};
+    g_subtype_val = new name{"Subtype", "val"};
+    g_subtype_rec = new name{"Subtype", "rec"};
+    g_psum = new name{"Psum"};
+    g_psum_cases_on = new name{"Psum", "casesOn"};
+    g_psum_inl = new name{"Psum", "inl"};
+    g_psum_inr = new name{"Psum", "inr"};
     g_tactic = new name{"tactic"};
     g_tactic_try = new name{"tactic", "try"};
     g_tactic_triv = new name{"tactic", "triv"};
-    g_tactic_mk_inj_eq = new name{"tactic", "mk_inj_eq"};
-    g_task = new name{"task"};
-    g_thunk = new name{"thunk"};
-    g_thunk_mk = new name{"thunk", "mk"};
-    g_trans_rel_left = new name{"trans_rel_left"};
-    g_trans_rel_right = new name{"trans_rel_right"};
-    g_true = new name{"true"};
-    g_true_intro = new name{"true", "intro"};
-    g_typed_expr = new name{"typed_expr"};
+    g_tactic_mk_inj_eq = new name{"tactic", "mkInjEq"};
+    g_task = new name{"Task"};
+    g_thunk = new name{"Thunk"};
+    g_thunk_mk = new name{"Thunk", "mk"};
+    g_trans_rel_left = new name{"transRelLeft"};
+    g_trans_rel_right = new name{"transRelRight"};
+    g_true = new name{"True"};
+    g_true_intro = new name{"True", "intro"};
+    g_typed_expr = new name{"typedExpr"};
     g_unit = new name{"unit"};
     g_unit_star = new name{"unit", "star"};
-    g_monad_from_pure_bind = new name{"monad_from_pure_bind"};
-    g_uint8 = new name{"uint8"};
-    g_uint16 = new name{"uint16"};
-    g_uint32 = new name{"uint32"};
-    g_uint64 = new name{"uint64"};
-    g_usize = new name{"usize"};
-    g_user_attribute = new name{"user_attribute"};
-    g_user_attribute_parse_reflect = new name{"user_attribute", "parse_reflect"};
-    g_well_founded_fix = new name{"well_founded", "fix"};
-    g_well_founded_fix_eq = new name{"well_founded", "fix_eq"};
-    g_well_founded_tactics = new name{"well_founded_tactics"};
-    g_well_founded_tactics_default = new name{"well_founded_tactics", "default"};
-    g_well_founded_tactics_rel_tac = new name{"well_founded_tactics", "rel_tac"};
-    g_well_founded_tactics_dec_tac = new name{"well_founded_tactics", "dec_tac"};
-    g_wf_term_hack = new name{"wf_term_hack"};
+    g_monad_from_pure_bind = new name{"monadFromPureBind"};
+    g_uint8 = new name{"Uint8"};
+    g_uint16 = new name{"Uint16"};
+    g_uint32 = new name{"Uint32"};
+    g_uint64 = new name{"Uint64"};
+    g_usize = new name{"Usize"};
+    g_user_attribute = new name{"userAttribute"};
+    g_user_attribute_parse_reflect = new name{"userAttribute", "parseReflect"};
+    g_well_founded_fix = new name{"WellFounded", "fix"};
+    g_well_founded_fix_eq = new name{"WellFounded", "fixEq"};
+    g_well_founded_tactics = new name{"wellFoundedTactics"};
+    g_well_founded_tactics_default = new name{"wellFoundedTactics", "default"};
+    g_well_founded_tactics_rel_tac = new name{"wellFoundedTactics", "relTac"};
+    g_well_founded_tactics_dec_tac = new name{"wellFoundedTactics", "decTac"};
+    g_wf_term_hack = new name{"wfTermHack"};
 }
 void finalize_constants() {
     delete g_absurd;
@@ -591,15 +591,15 @@ void finalize_constants() {
     delete g_bool;
     delete g_bool_ff;
     delete g_bool_tt;
-    delete g_combinator_K;
+    delete g_combinator_k;
     delete g_cast;
     delete g_char;
     delete g_char_mk;
     delete g_char_ne_of_vne;
     delete g_char_of_nat;
     delete g_char_of_nat_ne_of_ne;
-    delete g_is_valid_char_range_1;
-    delete g_is_valid_char_range_2;
+    delete g_is_valid_char_range1;
+    delete g_is_valid_char_range2;
     delete g_coe;
     delete g_coe_fn;
     delete g_coe_sort;
@@ -614,7 +614,7 @@ void finalize_constants() {
     delete g_decidable_is_false;
     delete g_dite;
     delete g_empty;
-    delete g_Exists;
+    delete g_exists;
     delete g_eq;
     delete g_eq_cases_on;
     delete g_eq_rec_on;
@@ -875,15 +875,15 @@ name const & get_bin_tree_node_name() { return *g_bin_tree_node; }
 name const & get_bool_name() { return *g_bool; }
 name const & get_bool_ff_name() { return *g_bool_ff; }
 name const & get_bool_tt_name() { return *g_bool_tt; }
-name const & get_combinator_K_name() { return *g_combinator_K; }
+name const & get_combinator_k_name() { return *g_combinator_k; }
 name const & get_cast_name() { return *g_cast; }
 name const & get_char_name() { return *g_char; }
 name const & get_char_mk_name() { return *g_char_mk; }
 name const & get_char_ne_of_vne_name() { return *g_char_ne_of_vne; }
 name const & get_char_of_nat_name() { return *g_char_of_nat; }
 name const & get_char_of_nat_ne_of_ne_name() { return *g_char_of_nat_ne_of_ne; }
-name const & get_is_valid_char_range_1_name() { return *g_is_valid_char_range_1; }
-name const & get_is_valid_char_range_2_name() { return *g_is_valid_char_range_2; }
+name const & get_is_valid_char_range1_name() { return *g_is_valid_char_range1; }
+name const & get_is_valid_char_range2_name() { return *g_is_valid_char_range2; }
 name const & get_coe_name() { return *g_coe; }
 name const & get_coe_fn_name() { return *g_coe_fn; }
 name const & get_coe_sort_name() { return *g_coe_sort; }
@@ -898,7 +898,7 @@ name const & get_decidable_is_true_name() { return *g_decidable_is_true; }
 name const & get_decidable_is_false_name() { return *g_decidable_is_false; }
 name const & get_dite_name() { return *g_dite; }
 name const & get_empty_name() { return *g_empty; }
-name const & get_Exists_name() { return *g_Exists; }
+name const & get_exists_name() { return *g_exists; }
 name const & get_eq_name() { return *g_eq; }
 name const & get_eq_cases_on_name() { return *g_eq_cases_on; }
 name const & get_eq_rec_on_name() { return *g_eq_rec_on; }
diff --git a/src/library/constants.h b/src/library/constants.h
index 904114aa41..02f06b7443 100644
--- a/src/library/constants.h
+++ b/src/library/constants.h
@@ -24,15 +24,15 @@ name const & get_bin_tree_node_name();
 name const & get_bool_name();
 name const & get_bool_ff_name();
 name const & get_bool_tt_name();
-name const & get_combinator_K_name();
+name const & get_combinator_k_name();
 name const & get_cast_name();
 name const & get_char_name();
 name const & get_char_mk_name();
 name const & get_char_ne_of_vne_name();
 name const & get_char_of_nat_name();
 name const & get_char_of_nat_ne_of_ne_name();
-name const & get_is_valid_char_range_1_name();
-name const & get_is_valid_char_range_2_name();
+name const & get_is_valid_char_range1_name();
+name const & get_is_valid_char_range2_name();
 name const & get_coe_name();
 name const & get_coe_fn_name();
 name const & get_coe_sort_name();
@@ -47,7 +47,7 @@ name const & get_decidable_is_true_name();
 name const & get_decidable_is_false_name();
 name const & get_dite_name();
 name const & get_empty_name();
-name const & get_Exists_name();
+name const & get_exists_name();
 name const & get_eq_name();
 name const & get_eq_cases_on_name();
 name const & get_eq_rec_on_name();
diff --git a/src/library/constructions/brec_on.cpp b/src/library/constructions/brec_on.cpp
index c71d87375f..6374a555c8 100644
--- a/src/library/constructions/brec_on.cpp
+++ b/src/library/constructions/brec_on.cpp
@@ -14,6 +14,7 @@ Author: Leonardo de Moura
 #include "library/reducible.h"
 #include "library/module.h"
 #include "library/bin_app.h"
+#include "library/suffixes.h"
 #include "library/util.h"
 #include "library/aux_recursors.h"
 #include "library/constructions/util.h"
@@ -335,7 +336,7 @@ static environment mk_brec_on(environment const & env, name const & n, bool ind)
         rec = mk_app(rec, ref_args[i]);
 
     type_checker tc(env, lctx);
-    name brec_on_name  = name(n, ind ? "binduction_on" : "brec_on");
+    name brec_on_name  = name(n, ind ? g_binduction_on : g_brec_on);
     expr brec_on_type  = lctx.mk_pi(args, result_type);
     expr brec_on_value = lctx.mk_lambda(args, mk_pprod_fst(tc, rec, ind));
 
diff --git a/src/library/constructions/cases_on.cpp b/src/library/constructions/cases_on.cpp
index 58fad59ae5..e8fe012093 100644
--- a/src/library/constructions/cases_on.cpp
+++ b/src/library/constructions/cases_on.cpp
@@ -10,6 +10,7 @@ Author: Leonardo de Moura
 #include "kernel/abstract.h"
 #include "kernel/inductive.h"
 #include "library/module.h"
+#include "library/suffixes.h"
 #include "library/protected.h"
 #include "library/reducible.h"
 #include "library/constants.h"
@@ -43,8 +44,8 @@ static bool is_type_former_arg(buffer<name> const & C_ids, expr const & arg) {
 environment mk_cases_on(environment const & env, name const & n) {
     constant_info ind_info = env.get(n);
     if (!ind_info.is_inductive())
-        throw exception(sstream() << "error in 'cases_on' generation, '" << n << "' is not an inductive datatype");
-    name cases_on_name(n, "cases_on");
+        throw exception(sstream() << "error in '" << g_cases_on << "' generation, '" << n << "' is not an inductive datatype");
+    name cases_on_name(n, g_cases_on);
     local_ctx lctx;
     inductive_val ind_val  = ind_info.to_inductive_val();
     name_generator ngen    = mk_constructions_name_generator();
diff --git a/src/library/constructions/no_confusion.cpp b/src/library/constructions/no_confusion.cpp
index 8801d0a2f1..cce434667c 100644
--- a/src/library/constructions/no_confusion.cpp
+++ b/src/library/constructions/no_confusion.cpp
@@ -12,6 +12,7 @@ Author: Leonardo de Moura
 #include "library/protected.h"
 #include "library/module.h"
 #include "library/util.h"
+#include "library/suffixes.h"
 #include "library/reducible.h"
 #include "library/constants.h"
 #include "library/aux_recursors.h"
@@ -19,7 +20,7 @@ Author: Leonardo de Moura
 
 namespace lean {
 static void throw_corrupted(name const & n) {
-    throw exception(sstream() << "error in 'no_confusion' generation, '" << n << "' inductive datatype declaration is corrupted");
+    throw exception(sstream() << "error in '" << g_no_confusion << "' generation, '" << n << "' inductive datatype declaration is corrupted");
 }
 
 static optional<environment> mk_no_confusion_type(environment const & env, name const & n) {
@@ -30,7 +31,7 @@ static optional<environment> mk_no_confusion_type(environment const & env, name
     local_ctx lctx;
     name_generator ngen      = mk_constructions_name_generator();
     unsigned nparams         = ind_val.get_nparams();
-    constant_info cases_info = env.get(name(n, "cases_on"));
+    constant_info cases_info = env.get(name(n, g_cases_on));
     names lps                = cases_info.get_lparams();
     level  plvl              = mk_univ_param(head(lps));
     levels ilvls             = lparams_to_levels(tail(lps));
@@ -56,7 +57,7 @@ static optional<environment> mk_no_confusion_type(environment const & env, name
     args.push_back(v2);
     expr R = mk_sort(rlvl);
     expr Pres = P;
-    name no_confusion_type_name{n, "no_confusion_type"};
+    name no_confusion_type_name{n, g_no_confusion_type};
     expr no_confusion_type_type = lctx.mk_pi(args, R);
     /* Create type former */
     buffer<expr> type_former_args;
@@ -135,8 +136,8 @@ environment mk_no_confusion(environment const & env, name const & n) {
     constant_info ind_info               = new_env.get(n);
     inductive_val ind_val                = ind_info.to_inductive_val();
     unsigned nparams                     = ind_val.get_nparams();
-    constant_info no_confusion_type_info = new_env.get(name{n, "no_confusion_type"});
-    constant_info cases_info             = new_env.get(name(n, "cases_on"));
+    constant_info no_confusion_type_info = new_env.get(name{n, g_no_confusion_type});
+    constant_info cases_info             = new_env.get(name(n, g_cases_on));
     names lps                            = no_confusion_type_info.get_lparams();
     levels ls                            = lparams_to_levels(lps);
     expr ind_type                        = instantiate_type_lparams(ind_info, tail(ls));
@@ -156,7 +157,7 @@ environment mk_no_confusion(environment const & env, name const & n) {
     expr eq_v         = mk_app(mk_constant(get_eq_name(), levels(v_lvl)), v_type);
     expr H12          = lctx.mk_local_decl(ngen, "h12", mk_app(eq_v, v1, v2), mk_binder_info());
     args.push_back(H12);
-    name no_confusion_name{n, "no_confusion"};
+    name no_confusion_name{n, g_no_confusion};
     expr no_confusion_ty = lctx.mk_pi(args, range);
     // The gen proof is of the form
     //   (fun H11 : v1 = v1, cases_on Params (fun Indices v1, no_confusion_type Params Indices P v1 v1) Indices v1
diff --git a/src/library/constructions/rec_on.cpp b/src/library/constructions/rec_on.cpp
index f5f3062056..83cf7792cd 100644
--- a/src/library/constructions/rec_on.cpp
+++ b/src/library/constructions/rec_on.cpp
@@ -12,6 +12,7 @@ Author: Leonardo de Moura
 #include "library/module.h"
 #include "library/reducible.h"
 #include "library/protected.h"
+#include "library/suffixes.h"
 #include "library/aux_recursors.h"
 #include "library/constructions/util.h"
 
@@ -19,10 +20,10 @@ namespace lean {
 environment mk_rec_on(environment const & env, name const & n) {
     constant_info ind_info = env.get(n);
     if (!ind_info.is_inductive())
-        throw exception(sstream() << "error in 'rec_on' generation, '" << n << "' is not an inductive datatype");
+        throw exception(sstream() << "error in '" << g_rec_on << "' generation, '" << n << "' is not an inductive datatype");
     name_generator ngen = mk_constructions_name_generator();
     local_ctx lctx;
-    name rec_on_name(n, "rec_on");
+    name rec_on_name(n, g_rec_on);
     constant_info rec_info = env.get(mk_rec_name(n));
     recursor_val  rec_val  = rec_info.to_recursor_val();
     buffer<expr> locals;
diff --git a/src/library/equations_compiler/structural_rec.cpp b/src/library/equations_compiler/structural_rec.cpp
index 47ba2899d4..4d2df40105 100644
--- a/src/library/equations_compiler/structural_rec.cpp
+++ b/src/library/equations_compiler/structural_rec.cpp
@@ -11,6 +11,7 @@ Author: Leonardo de Moura
 #include "library/locals.h"
 #include "library/class.h"
 #include "library/util.h"
+#include "library/suffixes.h"
 #include "library/pattern_attribute.h"
 #include "library/app_builder.h"
 #include "library/replace_visitor_with_tc.h"
@@ -225,7 +226,7 @@ struct structural_rec_fn {
         name I_name   = const_name(I);
         inductive_val I_val = m_env.get(I_name).to_inductive_val();
         m_reflexive   = I_val.is_reflexive();
-        if (!m_env.find(name(I_name, "brec_on"))) {
+        if (!m_env.find(name(I_name, g_brec_on))) {
             trace_struct(tout() << "structural recursion on argument #" << (arg_idx+1) << " was not used "
                          << "for '" << fn << "' because the inductive type '" << I << "' does have brec_on recursor\n  "
                          << arg_type << "\n";);
@@ -550,8 +551,8 @@ struct structural_rec_fn {
     }
 
     void update_eqs(type_context_old & ctx, unpack_eqns & ues, expr const & fn, expr const & new_fn) {
-        /* C is a temporary "abstract" motive, we use it to access the "brec_on dictionary".
-           The "brec_on dictionary is an element of type below, and it is the last argument of the new function. */
+        /* C is a temporary "abstract" motive, we use it to access the "g_brec_on dictionary".
+           The g_brec_on dictionary is an element of type below, and it is the last argument of the new function. */
         expr C = mk_local(ctx.next_name(), "_C", m_motive_type, mk_binder_info());
         buffer<expr> & eqns = ues.get_eqns_of(0);
         buffer<expr> new_eqns;
@@ -677,7 +678,7 @@ struct structural_rec_fn {
         buffer<expr> below_args;
         expr below        = get_app_args(below_type, below_args);
         expr motive       = below_args[nparams];
-        name brec_on_name = name(I_name, m_use_ibelow ? "binduction_on" : "brec_on");
+        name brec_on_name = name(I_name, m_use_ibelow ? g_binduction_on : g_brec_on);
         expr brec_on_fn   = mk_constant(brec_on_name, const_levels(below));
         buffer<expr> brec_on_args;
         buffer<expr> F_domain; /* domain for F argument for brec_on */
diff --git a/src/library/suffixes.h b/src/library/suffixes.h
new file mode 100644
index 0000000000..06144335fc
--- /dev/null
+++ b/src/library/suffixes.h
@@ -0,0 +1,17 @@
+/*
+Copyright (c) 2019 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+
+namespace lean {
+constexpr char const * g_rec               = "rec";
+constexpr char const * g_rec_on            = "recOn";
+constexpr char const * g_brec_on           = "brecOn";
+constexpr char const * g_binduction_on     = "binductionOn";
+constexpr char const * g_cases_on          = "casesOn";
+constexpr char const * g_no_confusion      = "noConfusion";
+constexpr char const * g_no_confusion_type = "noConfusionType";
+}
diff --git a/src/library/tactic/cases_tactic.cpp b/src/library/tactic/cases_tactic.cpp
index e881723ebc..6df1cd6427 100644
--- a/src/library/tactic/cases_tactic.cpp
+++ b/src/library/tactic/cases_tactic.cpp
@@ -12,6 +12,7 @@ Author: Leonardo de Moura
 #include "library/locals.h"
 #include "library/app_builder.h"
 #include "library/trace.h"
+#include "library/suffixes.h"
 #include "library/tactic/cases_tactic.h"
 #include "library/tactic/intro_tactic.h"
 #include "library/tactic/clear_tactic.h"
@@ -104,7 +105,7 @@ struct cases_tactic_fn {
             return false;
         if (!is_inductive(m_env, const_name(fn)))
             return false;
-        if (!m_env.find(name{const_name(fn), "cases_on"}) || !m_env.find(get_eq_name()))
+        if (!m_env.find(name{const_name(fn), g_cases_on}) || !m_env.find(get_eq_name()))
             return false;
         if (!m_env.find(get_heq_name()))
             return false;
@@ -386,7 +387,7 @@ struct cases_tactic_fn {
                     if (!A_info.is_inductive())
                         throw_ill_formed_datatype();
                     inductive_val A_val  = A_info.to_inductive_val();
-                    name no_confusion_name(const_name(A_fn), "no_confusion");
+                    name no_confusion_name(const_name(A_fn), g_no_confusion);
                     if (!m_env.find(no_confusion_name)) {
                         throw exception(sstream() << "cases tactic failed, construction '"
                                         << no_confusion_name << "' is not available in the environment");
diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp
index 09ece1fab4..cc4143dfc6 100644
--- a/src/library/type_context.cpp
+++ b/src/library/type_context.cpp
@@ -21,6 +21,7 @@ Author: Leonardo de Moura
 #include "library/annotation.h"
 #include "library/idx_metavar.h"
 #include "library/reducible.h"
+#include "library/suffixes.h"
 #include "library/constants.h"
 #include "library/metavar_util.h"
 #include "library/exception.h"
@@ -676,7 +677,7 @@ optional<expr> type_context_old::reduce_aux_recursor(expr const & e) {
            This fix is a little bit hackish and non modular because `brec_on` auxiliary recursors are defined in
            a completely different module, and type_context should not be aware of them.
         */
-        if (r && const_name(f).get_string() == "brec_on") {
+        if (r && const_name(f).get_string() == g_brec_on) {
             if (auto r2 = reduce_projection(*r))
                 return r2;
         }
diff --git a/src/library/user_recursors.cpp b/src/library/user_recursors.cpp
index f00e3dfecd..d4c6885d17 100644
--- a/src/library/user_recursors.cpp
+++ b/src/library/user_recursors.cpp
@@ -15,6 +15,7 @@ Author: Leonardo de Moura
 #include "library/user_recursors.h"
 #include "library/aux_recursors.h"
 #include "library/attribute_manager.h"
+#include "library/suffixes.h"
 
 namespace lean {
 bool recursor_info::is_minor(unsigned pos) const {
@@ -107,16 +108,16 @@ recursor_info mk_recursor_info(environment const & env, name const & r, optional
         return recursor_info(r, I_name, universe_pos, has_dep_elim, is_rec,
                              num_args, major_pos, params_pos, indices_pos, produce_motive);
     } else if (is_aux_recursor(env, r) &&
-               (r.get_string() == "cases_on" ||
-                r.get_string() == "rec_on"   ||
-                r.get_string() == "brec_on")) {
+               (r.get_string() == g_cases_on ||
+                r.get_string() == g_rec_on   ||
+                r.get_string() == g_brec_on)) {
         name I_name           = r.get_prefix();
         inductive_val I_val   = env.get(I_name).to_inductive_val();
         unsigned num_indices  = I_val.get_nindices();
         unsigned num_params   = I_val.get_nparams();
         has_given_major_pos   = true;
         unsigned num_motives;
-        if (r.get_string() == "cases_on") {
+        if (r.get_string() == g_cases_on) {
             num_motives = 1;
         } else {
             num_motives = env.get(mk_rec_name(I_name)).to_recursor_val().get_nmotives();
diff --git a/src/library/util.cpp b/src/library/util.cpp
index d806f55e24..60f238243f 100644
--- a/src/library/util.cpp
+++ b/src/library/util.cpp
@@ -16,6 +16,7 @@ Author: Leonardo de Moura
 #include "library/error_msgs.h"
 #include "library/locals.h"
 #include "library/util.h"
+#include "library/suffixes.h"
 #include "library/annotation.h"
 #include "library/constants.h"
 #include "library/pp_options.h"
@@ -818,7 +819,7 @@ expr mk_absurd(abstract_type_context & ctx, expr const & t, expr const & e, expr
 }
 
 bool is_exists(expr const & e, expr & A, expr & p) {
-    if (is_app_of(e, get_Exists_name(), 2)) {
+    if (is_app_of(e, get_exists_name(), 2)) {
         A = app_arg(app_fn(e));
         p = app_arg(e);
         return true;
@@ -828,7 +829,7 @@ bool is_exists(expr const & e, expr & A, expr & p) {
 }
 
 bool is_exists(expr const & e) {
-    return is_app_of(e, get_Exists_name(), 2);
+    return is_app_of(e, get_exists_name(), 2);
 }
 
 optional<expr> get_binary_op(expr const & e) {
@@ -984,11 +985,11 @@ expr mk_bool_ff() { return *g_bool_ff; }
 expr to_bool_expr(bool b) { return b ? mk_bool_tt() : mk_bool_ff(); }
 
 name get_dep_recursor(environment const &, name const & n) {
-    return name(n, "rec");
+    return name(n, g_rec);
 }
 
 name get_dep_cases_on(environment const &, name const & n) {
-    return name(n, "cases_on");
+    return name(n, g_cases_on);
 }
 
 static char const * g_unsafe_rec_prefix = "_unsafe_rec";