diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el
index 7ed655112..f408154e7 100644
--- a/src/emacs/lean-syntax.el
+++ b/src/emacs/lean-syntax.el
@@ -118,7 +118,8 @@
      (,(rx symbol-start "_" symbol-end) . 'font-lock-preprocessor-face)
      ;; modifiers
      (,(rx (or "\[persistent\]" "\[notation\]" "\[visible\]" "\[instance\]" "\[class\]" "\[parsing-only\]"
-               "\[coercion\]" "\[reducible\]" "\[irreducible\]" "\[wf\]" "\[whnf\]" "\[multiple-instances\]"
+               "\[coercion\]" "\[reducible\]" "\[irreducible\]" "\[semireducible\]" "\[wf\]"
+               "\[whnf\]" "\[multiple-instances\]"
                "\[decls\]" "\[declarations\]" "\[all-transparent\]" "\[coercions\]" "\[classes\]"
                "\[notations\]" "\[abbreviations\]" "\[begin-end-hints\]" "\[tactic-hints\]" "\[reduce-hints\]"))
       . 'font-lock-doc-face)
diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp
index af8ca6805..d8281206c 100644
--- a/src/frontends/lean/decl_cmds.cpp
+++ b/src/frontends/lean/decl_cmds.cpp
@@ -290,6 +290,7 @@ struct decl_attributes {
     bool               m_is_coercion;
     bool               m_is_reducible;
     bool               m_is_irreducible;
+    bool               m_is_semireducible;
     bool               m_is_class;
     bool               m_is_parsing_only;
     bool               m_has_multiple_instances;
@@ -303,6 +304,7 @@ struct decl_attributes {
         m_is_coercion            = false;
         m_is_reducible           = is_abbrev;
         m_is_irreducible         = false;
+        m_is_semireducible       = false;
         m_is_class               = false;
         m_is_parsing_only        = false;
         m_has_multiple_instances = false;
@@ -361,15 +363,20 @@ struct decl_attributes {
                     throw parser_error("invalid '[coercion]' attribute, coercions cannot be defined in contexts", pos);
                 m_is_coercion = true;
             } else if (p.curr_is_token(get_reducible_tk())) {
-                if (m_is_irreducible)
-                    throw parser_error("invalid '[reducible]' attribute, '[irreducible]' was already provided", pos);
+                if (m_is_irreducible || m_is_semireducible)
+                    throw parser_error("invalid '[reducible]' attribute, '[irreducible]' or '[semireducible]' was already provided", pos);
                 m_is_reducible = true;
                 p.next();
             } else if (p.curr_is_token(get_irreducible_tk())) {
-                if (m_is_reducible)
-                    throw parser_error("invalid '[irreducible]' attribute, '[reducible]' was already provided", pos);
+                if (m_is_reducible || m_is_semireducible)
+                    throw parser_error("invalid '[irreducible]' attribute, '[reducible]' or '[semireducible]' was already provided", pos);
                 m_is_irreducible = true;
                 p.next();
+            } else if (p.curr_is_token(get_semireducible_tk())) {
+                if (m_is_reducible || m_is_irreducible)
+                    throw parser_error("invalid '[irreducible]' attribute, '[reducible]' or '[irreducible]' was already provided", pos);
+                m_is_semireducible = true;
+                p.next();
             } else if (p.curr_is_token(get_class_tk())) {
                 if (m_def_only)
                     throw parser_error("invalid '[class]' attribute, definitions cannot be marked as classes", pos);
@@ -417,9 +424,11 @@ struct decl_attributes {
         if (m_is_coercion)
             env = add_coercion(env, d, ios, persistent);
         if (m_is_reducible)
-            env = set_reducible(env, d, reducible_status::On, persistent);
+            env = set_reducible(env, d, reducible_status::Reducible, persistent);
         if (m_is_irreducible)
-            env = set_reducible(env, d, reducible_status::Off, persistent);
+            env = set_reducible(env, d, reducible_status::Irreducible, persistent);
+        if (m_is_semireducible)
+            env = set_reducible(env, d, reducible_status::Semireducible, persistent);
         if (m_is_class)
             env = add_class(env, d, persistent);
         if (m_has_multiple_instances)
diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp
index 66ad3e845..d2eddf253 100644
--- a/src/frontends/lean/structure_cmd.cpp
+++ b/src/frontends/lean/structure_cmd.cpp
@@ -722,7 +722,7 @@ struct structure_cmd_fn {
                                              rec_on_decl.get_type(), rec_on_decl.get_value(),
                                              opaque);
         m_env = module::add(m_env, check(m_env, new_decl));
-        m_env = set_reducible(m_env, n, reducible_status::On);
+        m_env = set_reducible(m_env, n, reducible_status::Reducible);
         save_def_info(n);
         add_alias(n);
     }
@@ -817,7 +817,7 @@ struct structure_cmd_fn {
             declaration coercion_decl      = mk_definition(m_env, coercion_name, lnames, coercion_type, coercion_value,
                                                            opaque);
             m_env = module::add(m_env, check(m_env, coercion_decl));
-            m_env = set_reducible(m_env, coercion_name, reducible_status::On);
+            m_env = set_reducible(m_env, coercion_name, reducible_status::Reducible);
             save_def_info(coercion_name);
             add_alias(coercion_name);
             if (!m_private_parents[i]) {
diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp
index 1a7cc2e40..2de066ec6 100644
--- a/src/frontends/lean/token_table.cpp
+++ b/src/frontends/lean/token_table.cpp
@@ -87,10 +87,13 @@ void init_token_table(token_table & t) {
          {"<d", g_decreasing_prec}, {"renaming", 0}, {"extends", 0}, {nullptr, 0}};
 
     char const * commands[] =
-        {"theorem", "axiom", "variable", "protected", "private", "opaque", "definition", "example", "coercion", "abbreviation",
+        {"theorem", "axiom", "variable", "protected", "private", "opaque", "definition", "example", "coercion",
+         "abbreviation",
          "variables", "parameter", "parameters", "constant", "constants", "[persistent]", "[visible]", "[instance]",
-         "[off]", "[on]", "[none]", "[class]", "[coercion]", "[reducible]", "[irreducible]", "[parsing-only]", "[multiple-instances]",
-         "evaluate", "check", "eval", "[wf]", "[whnf]", "[all-transparent]", "[priority", "[unfold-c", "print", "end", "namespace", "section", "prelude",
+         "[off]", "[on]", "[none]", "[class]", "[coercion]", "[reducible]", "[irreducible]", "[semireducible]",
+         "[parsing-only]", "[multiple-instances]",
+         "evaluate", "check", "eval", "[wf]", "[whnf]", "[all-transparent]", "[priority", "[unfold-c", "print",
+         "end", "namespace", "section", "prelude",
          "import", "inductive", "record", "structure", "module", "universe", "universes", "local",
          "precedence", "reserve", "infixl", "infixr", "infix", "postfix", "prefix", "notation", "context",
          "exit", "set_option", "open", "export", "calc_subst", "calc_refl", "calc_trans", "calc_symm", "tactic_hint",
diff --git a/src/frontends/lean/tokens.cpp b/src/frontends/lean/tokens.cpp
index eff3c52a2..8c5b59456 100644
--- a/src/frontends/lean/tokens.cpp
+++ b/src/frontends/lean/tokens.cpp
@@ -100,6 +100,7 @@ static name * g_priority     = nullptr;
 static name * g_unfold_c     = nullptr;
 static name * g_coercion     = nullptr;
 static name * g_reducible    = nullptr;
+static name * g_semireducible = nullptr;
 static name * g_irreducible  = nullptr;
 static name * g_parsing_only = nullptr;
 static name * g_with         = nullptr;
@@ -219,6 +220,7 @@ void initialize_tokens() {
     g_unfold_c     = new name("[unfold-c");
     g_coercion     = new name("[coercion]");
     g_reducible    = new name("[reducible]");
+    g_semireducible = new name("[semireducible]");
     g_irreducible  = new name("[irreducible]");
     g_parsing_only = new name("[parsing-only]");
     g_attribute    = new name("attribute");
@@ -280,6 +282,7 @@ void finalize_tokens() {
     delete g_unfold_c;
     delete g_coercion;
     delete g_reducible;
+    delete g_semireducible;
     delete g_irreducible;
     delete g_multiple_instances;
     delete g_attribute;
@@ -459,6 +462,7 @@ name const & get_priority_tk() { return *g_priority; }
 name const & get_unfold_c_tk() { return *g_unfold_c; }
 name const & get_coercion_tk() { return *g_coercion; }
 name const & get_reducible_tk() { return *g_reducible; }
+name const & get_semireducible_tk() { return *g_semireducible; }
 name const & get_irreducible_tk() { return *g_irreducible; }
 name const & get_multiple_instances_tk() { return *g_multiple_instances; }
 name const & get_attribute_tk() { return *g_attribute; }
diff --git a/src/frontends/lean/tokens.h b/src/frontends/lean/tokens.h
index 3fa950980..93a5fb2de 100644
--- a/src/frontends/lean/tokens.h
+++ b/src/frontends/lean/tokens.h
@@ -102,6 +102,7 @@ name const & get_priority_tk();
 name const & get_unfold_c_tk();
 name const & get_coercion_tk();
 name const & get_reducible_tk();
+name const & get_semireducible_tk();
 name const & get_irreducible_tk();
 name const & get_multiple_instances_tk();
 name const & get_attribute_tk();
diff --git a/src/library/definitional/brec_on.cpp b/src/library/definitional/brec_on.cpp
index c4b50602b..3c868213a 100644
--- a/src/library/definitional/brec_on.cpp
+++ b/src/library/definitional/brec_on.cpp
@@ -145,7 +145,7 @@ static environment mk_below(environment const & env, name const & n, bool ibelow
     declaration new_d = mk_definition(env, below_name, blvls, below_type, below_value,
                                       opaque, rec_decl.get_module_idx(), use_conv_opt);
     environment new_env = module::add(env, check(env, new_d));
-    new_env = set_reducible(new_env, below_name, reducible_status::On);
+    new_env = set_reducible(new_env, below_name, reducible_status::Reducible);
     return add_protected(new_env, below_name);
 }
 
@@ -330,7 +330,7 @@ static environment mk_brec_on(environment const & env, name const & n, bool ind)
     declaration new_d = mk_definition(env, brec_on_name, blps, brec_on_type, brec_on_value,
                                       opaque, rec_decl.get_module_idx(), use_conv_opt);
     environment new_env = module::add(env, check(env, new_d));
-    new_env = set_reducible(new_env, brec_on_name, reducible_status::On);
+    new_env = set_reducible(new_env, brec_on_name, reducible_status::Reducible);
     return add_protected(new_env, brec_on_name);
 }
 
diff --git a/src/library/definitional/cases_on.cpp b/src/library/definitional/cases_on.cpp
index 2a2ccb8c0..85fe3398e 100644
--- a/src/library/definitional/cases_on.cpp
+++ b/src/library/definitional/cases_on.cpp
@@ -180,7 +180,7 @@ environment mk_cases_on(environment const & env, name const & n) {
     declaration new_d = mk_definition(env, cases_on_name, rec_decl.get_univ_params(), cases_on_type, cases_on_value,
                                       opaque, rec_decl.get_module_idx(), use_conv_opt);
     environment new_env = module::add(env, check(env, new_d));
-    new_env = set_reducible(new_env, cases_on_name, reducible_status::On);
+    new_env = set_reducible(new_env, cases_on_name, reducible_status::Reducible);
     return add_protected(new_env, cases_on_name);
 }
 }
diff --git a/src/library/definitional/no_confusion.cpp b/src/library/definitional/no_confusion.cpp
index 0995b2735..ebba06f6a 100644
--- a/src/library/definitional/no_confusion.cpp
+++ b/src/library/definitional/no_confusion.cpp
@@ -139,7 +139,7 @@ optional<environment> mk_no_confusion_type(environment const & env, name const &
     declaration new_d = mk_definition(env, no_confusion_type_name, lps, no_confusion_type_type, no_confusion_type_value,
                                       opaque, ind_decl.get_module_idx(), use_conv_opt);
     environment new_env = module::add(env, check(env, new_d));
-    new_env = set_reducible(new_env, no_confusion_type_name, reducible_status::On);
+    new_env = set_reducible(new_env, no_confusion_type_name, reducible_status::Reducible);
     return some(add_protected(new_env, no_confusion_type_name));
 }
 
@@ -274,7 +274,7 @@ environment mk_no_confusion(environment const & env, name const & n) {
     declaration new_d = mk_definition(new_env, no_confusion_name, lps, no_confusion_ty, no_confusion_val,
                                       opaque, no_confusion_type_decl.get_module_idx(), use_conv_opt);
     new_env = module::add(new_env, check(new_env, new_d));
-    new_env = set_reducible(new_env, no_confusion_name, reducible_status::On);
+    new_env = set_reducible(new_env, no_confusion_name, reducible_status::Reducible);
     return add_protected(new_env, no_confusion_name);
 }
 }
diff --git a/src/library/definitional/projection.cpp b/src/library/definitional/projection.cpp
index 4ada6bc07..707f5c5d7 100644
--- a/src/library/definitional/projection.cpp
+++ b/src/library/definitional/projection.cpp
@@ -134,7 +134,7 @@ environment mk_projections(environment const & env, name const & n, buffer<name>
         declaration new_d = mk_definition(env, proj_name, lvl_params, proj_type, proj_val,
                                           opaque, rec_decl.get_module_idx(), use_conv_opt);
         new_env = module::add(new_env, check(new_env, new_d));
-        new_env = set_reducible(new_env, proj_name, reducible_status::On);
+        new_env = set_reducible(new_env, proj_name, reducible_status::Reducible);
         new_env = add_unfold_c_hint(new_env, proj_name, nparams);
         new_env = save_projection_info(new_env, proj_name, inductive::intro_rule_name(intro), nparams, i, inst_implicit);
         expr proj         = mk_app(mk_app(mk_constant(proj_name, lvls), params), c);
diff --git a/src/library/definitional/rec_on.cpp b/src/library/definitional/rec_on.cpp
index c2cd74976..4554a1c40 100644
--- a/src/library/definitional/rec_on.cpp
+++ b/src/library/definitional/rec_on.cpp
@@ -57,7 +57,7 @@ environment mk_rec_on(environment const & env, name const & n) {
                                       check(env, mk_definition(env, rec_on_name, rec_decl.get_univ_params(),
                                                                rec_on_type, rec_on_val,
                                                                opaque, rec_decl.get_module_idx(), use_conv_opt)));
-    new_env = set_reducible(new_env, rec_on_name, reducible_status::On);
+    new_env = set_reducible(new_env, rec_on_name, reducible_status::Reducible);
     return add_protected(new_env, rec_on_name);
 }
 }
diff --git a/src/library/reducible.cpp b/src/library/reducible.cpp
index e6134aa48..beab1e269 100644
--- a/src/library/reducible.cpp
+++ b/src/library/reducible.cpp
@@ -17,7 +17,7 @@ namespace lean {
 struct reducible_entry {
     reducible_status m_status;
     name             m_name;
-    reducible_entry():m_status(reducible_status::None) {}
+    reducible_entry():m_status(reducible_status::Semireducible) {}
     reducible_entry(reducible_status s, name const & n):m_status(s), m_name(n) {}
 };
 
@@ -27,15 +27,15 @@ struct reducible_state {
 
     void add(reducible_entry const & e) {
         switch (e.m_status) {
-        case reducible_status::On:
+        case reducible_status::Reducible:
             m_reducible_on.insert(e.m_name);
             m_reducible_off.erase(e.m_name);
             break;
-        case reducible_status::Off:
+        case reducible_status::Irreducible:
             m_reducible_on.erase(e.m_name);
             m_reducible_off.insert(e.m_name);
             break;
-        case reducible_status::None:
+        case reducible_status::Semireducible:
             m_reducible_on.erase(e.m_name);
             m_reducible_off.erase(e.m_name);
             break;
@@ -221,9 +221,9 @@ static int set_reducible(lua_State * L) {
 
 void open_reducible(lua_State * L) {
     lua_newtable(L);
-    SET_ENUM("On",      reducible_status::On);
-    SET_ENUM("Off",     reducible_status::Off);
-    SET_ENUM("None",    reducible_status::None);
+    SET_ENUM("On",      reducible_status::Reducible);
+    SET_ENUM("Off",     reducible_status::Irreducible);
+    SET_ENUM("None",    reducible_status::Semireducible);
     lua_setglobal(L, "reducible_status");
     SET_GLOBAL_FUN(is_reducible_on,                 "is_reducible_on");
     SET_GLOBAL_FUN(is_reducible_off,                "is_reducible_off");
diff --git a/src/library/reducible.h b/src/library/reducible.h
index d719658c8..451219f4d 100644
--- a/src/library/reducible.h
+++ b/src/library/reducible.h
@@ -10,7 +10,7 @@ Author: Leonardo de Moura
 #include "kernel/default_converter.h"
 
 namespace lean {
-enum class reducible_status { On, Off, None };
+enum class reducible_status { Reducible, Irreducible, Semireducible };
 /** \brief Mark the definition named \c n as reducible or not.
 
     The method throws an exception if \c n is
diff --git a/tests/lean/red.lean b/tests/lean/red.lean
new file mode 100644
index 000000000..3db428b71
--- /dev/null
+++ b/tests/lean/red.lean
@@ -0,0 +1,26 @@
+constant g : nat → nat
+
+definition f := g
+
+example : f = g := rfl
+
+attribute f [irreducible]
+
+example : f = g := rfl  -- Error
+
+example (a : nat) (H : a = g a) : f a = a :=
+eq.subst H rfl -- Error
+
+attribute f [semireducible]
+
+example (a : nat) (H : a = g a) : f a = a :=
+eq.subst H rfl -- Error
+
+example : f = g := rfl
+
+attribute f [reducible]
+
+example : f = g := rfl
+
+example (a : nat) (H : a = g a) : f a = a :=
+eq.subst H rfl
diff --git a/tests/lean/red.lean.expected.out b/tests/lean/red.lean.expected.out
new file mode 100644
index 000000000..4a7d5b669
--- /dev/null
+++ b/tests/lean/red.lean.expected.out
@@ -0,0 +1,20 @@
+red.lean:9:19: error: type mismatch at definition '14.1', has type
+  f = f
+but is expected to have type
+  f = g
+red.lean:12:0: error: type mismatch at application
+  eq.subst H rfl
+term
+  rfl
+has type
+  f ?M_1 = f ?M_1
+but is expected to have type
+  f ?M_1 = a
+red.lean:17:0: error: type mismatch at application
+  eq.subst H rfl
+term
+  rfl
+has type
+  f ?M_1 = f ?M_1
+but is expected to have type
+  f ?M_1 = a