From 89e852446a7a83f0117b00a8dafd800638de7d25 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 4 Sep 2016 18:30:26 -0700
Subject: [PATCH] feat(library/init/id_locked): add auxiliary definition
 id_locked

---
 library/init/default.lean   |  2 +-
 library/init/id_locked.lean | 24 ++++++++++++++++++++++++
 2 files changed, 25 insertions(+), 1 deletion(-)
 create mode 100644 library/init/id_locked.lean

diff --git a/library/init/default.lean b/library/init/default.lean
index ad412bd4da..df9b1fc5f9 100644
--- a/library/init/default.lean
+++ b/library/init/default.lean
@@ -13,4 +13,4 @@ import init.monad_combinators
 import init.timeit init.trace init.unsigned init.ordering init.list_classes init.coe
 import init.wf init.nat_div init.meta init.instances
 import init.wf_k init.sigma_lex
-import init.simplifier
+import init.simplifier init.id_locked
diff --git a/library/init/id_locked.lean b/library/init/id_locked.lean
new file mode 100644
index 0000000000..1f93348a8d
--- /dev/null
+++ b/library/init/id_locked.lean
@@ -0,0 +1,24 @@
+/-
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import init.meta.tactic init.meta.constructor_tactic
+open tactic
+
+/-
+  Define id_locked using meta-programming because we don't have
+  syntax for setting reducibility_hints.
+
+  See module init.meta.declaration.
+-/
+run_command do
+ l  ← return $ level.param `l,
+ Ty ← return $ expr.sort l,
+ type ← to_expr `(Π {A : %%Ty}, A → A),
+ val  ← to_expr `(λ {A : %%Ty} (a : A), a),
+ add_decl (declaration.defn `id_locked [`l] type val reducibility_hints.opaque tt)
+
+lemma id_locked_eq {A : Type} (a : A) : id_locked a = a :=
+rfl