diff --git a/stage0/src/Init/Core.lean b/stage0/src/Init/Core.lean
index e113f1e2e0..627e2e6ce8 100644
--- a/stage0/src/Init/Core.lean
+++ b/stage0/src/Init/Core.lean
@@ -1707,6 +1707,35 @@ Quot.lift f (fun a b _ => Subsingleton.elim _ _) s
 instance Squash.Subsingleton {α} : Subsingleton (Squash α) :=
 ⟨Squash.ind (fun (a : α) => Squash.ind (fun (b : α) => Quot.sound trivial))⟩
 
+namespace Lean
+/- Kernel reduction hints -/
+
+/--
+  When the kernel tries to reduce a term `Lean.reduceBool c`, it will invoke the Lean interpreter to evaluate `c`.
+  The kernel will produce an error message if `c` is not a constant.
+  This feature is useful for performing proofs by reflection.
+
+  Remark: the Lean frontend allows terms of the from `Lean.reduceBool t` where `t` is a term not containing
+  free variables. The frontend automatically declares a fresh auxiliary constant `c` and replaces the term with
+  `Lean.reduceBool c`. The main motivation is that the code for `t` will be pre-compiled.
+
+  Warning: by using this feature, the Lean compiler and interpreter become part of your trusted code base.
+  This is extra 30k lines of code. More importantly, you will probably not be able to check your developement using
+  external type checkers (e.g., Trepplein) that do not implement this feature.
+  Keep in mind that if you are using Lean as programming language, you are already trusting the Lean compiler and interpreter.
+  So, you are mainly losing the capability of type checking your developement using external checkers. -/
+def reduceBool (b : Bool) : Bool := b
+
+/--
+  Similar to `Lean.reduceBool` for closed `Nat` terms.
+
+  Remark: we do not have plans for supporting a generic `reduceValue {α} (a : α) : α := a`.
+  The main issue is that it is non-trivial to convert an arbitrary runtime object back into a Lean expression.
+  We believe `Lean.reduceBool` enables most interesting applications (e.g., proof by reflection). -/
+def reduceNat (n : Nat) : Nat := n
+
+end Lean
+
 /- Classical reasoning support -/
 
 namespace Classical
diff --git a/stage0/stdlib/Init/Core.c b/stage0/stdlib/Init/Core.c
index 65aaa28437..8503da9efe 100644
--- a/stage0/stdlib/Init/Core.c
+++ b/stage0/stdlib/Init/Core.c
@@ -23,6 +23,7 @@ lean_object* l_Subtype_sizeof(lean_object*);
 lean_object* l_Quotient_hrecOn___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Quotient_lift(lean_object*, lean_object*, lean_object*);
 lean_object* l_Prod_DecidableEq___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
+uint8_t l_Lean_reduceBool(uint8_t);
 lean_object* l_inline(lean_object*);
 lean_object* l_Quotient_lift_u2082(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_condEq___rarg___boxed(lean_object*, lean_object*, lean_object*);
@@ -42,6 +43,7 @@ lean_object* l_Quotient_lift___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Squash_mk___rarg___boxed(lean_object*);
 lean_object* l_Nat_HasOne;
 lean_object* l_idRhs___rarg___boxed(lean_object*);
+lean_object* l_Lean_reduceBool___boxed(lean_object*);
 lean_object* l_arbitrary___rarg___boxed(lean_object*);
 lean_object* l_absurd(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_List_sizeof___main(lean_object*);
@@ -129,6 +131,7 @@ lean_object* l_Function_const___rarg___boxed(lean_object*, lean_object*);
 lean_object* l_setoidHasEquiv(lean_object*, lean_object*);
 lean_object* l_PUnit_sizeof(lean_object*);
 lean_object* l_Iff_Decidable(lean_object*, lean_object*);
+lean_object* l_Lean_reduceNat(lean_object*);
 lean_object* l_Nat_HasSizeof;
 lean_object* l_Squash_lift___rarg(lean_object*, lean_object*);
 lean_object* l_Ne_Decidable___rarg___boxed(lean_object*, lean_object*, lean_object*);
@@ -270,6 +273,7 @@ lean_object* l_Option_HasSizeof(lean_object*);
 lean_object* l_PSum_HasSizeof(lean_object*, lean_object*);
 lean_object* l_Function_const(lean_object*, lean_object*);
 lean_object* l_PUnit_Inhabited;
+lean_object* l_Lean_reduceNat___boxed(lean_object*);
 lean_object* l_Sum_HasSizeof(lean_object*, lean_object*);
 lean_object* l_Option_sizeof___rarg(lean_object*, lean_object*);
 lean_object* l_Eq_ndrecOn___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -3619,6 +3623,39 @@ x_4 = lean_alloc_closure((void*)(l_Squash_lift___rarg), 2, 0);
 return x_4;
 }
 }
+uint8_t l_Lean_reduceBool(uint8_t x_1) {
+_start:
+{
+return x_1;
+}
+}
+lean_object* l_Lean_reduceBool___boxed(lean_object* x_1) {
+_start:
+{
+uint8_t x_2; uint8_t x_3; lean_object* x_4; 
+x_2 = lean_unbox(x_1);
+lean_dec(x_1);
+x_3 = l_Lean_reduceBool(x_2);
+x_4 = lean_box(x_3);
+return x_4;
+}
+}
+lean_object* l_Lean_reduceNat(lean_object* x_1) {
+_start:
+{
+lean_inc(x_1);
+return x_1;
+}
+}
+lean_object* l_Lean_reduceNat___boxed(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = l_Lean_reduceNat(x_1);
+lean_dec(x_1);
+return x_2;
+}
+}
 static bool _G_initialized = false;
 lean_object* initialize_Init_Core(lean_object* w) {
 lean_object * res;