From 741fca1e7b86b2025083f4cfc82d70ab956f0ecf Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 4 May 2015 14:29:22 -0700
Subject: [PATCH] feat(hott/init/path): mark 'idp' and 'idpath' with
 '[unfold-m]' hint

closes #496
---
 hott/init/path.hlean                   |  4 ++--
 tests/lean/simp_idp.hlean              | 10 ++++++++++
 tests/lean/simp_idp.hlean.expected.out |  8 ++++++++
 3 files changed, 20 insertions(+), 2 deletions(-)
 create mode 100644 tests/lean/simp_idp.hlean
 create mode 100644 tests/lean/simp_idp.hlean.expected.out

diff --git a/hott/init/path.hlean b/hott/init/path.hlean
index 282aef345..6d85123f8 100644
--- a/hott/init/path.hlean
+++ b/hott/init/path.hlean
@@ -20,8 +20,8 @@ namespace eq
 
   --notation a = b := eq a b
   notation x = y `:>`:50 A:49 := @eq A x y
-  definition idp [reducible] {a : A} := refl a
-  definition idpath [reducible] (a : A) := refl a
+  definition idp [reducible] [unfold-m] {a : A} := refl a
+  definition idpath [reducible] [unfold-m] (a : A) := refl a
 
   -- unbased path induction
   definition rec' [reducible] {P : Π (a b : A), (a = b) -> Type}
diff --git a/tests/lean/simp_idp.hlean b/tests/lean/simp_idp.hlean
new file mode 100644
index 000000000..bd969b5ec
--- /dev/null
+++ b/tests/lean/simp_idp.hlean
@@ -0,0 +1,10 @@
+open eq
+
+example (A : Type) (C : A → Type) (a : A) (f g : C a → C a) (c : C a) : f = g → f (eq.rec_on idp c) = g c :=
+begin
+  intros,
+  esimp,
+  state, -- simplified goal to f c = g c
+  congruence,
+  assumption
+end
diff --git a/tests/lean/simp_idp.hlean.expected.out b/tests/lean/simp_idp.hlean.expected.out
new file mode 100644
index 000000000..cf47736e6
--- /dev/null
+++ b/tests/lean/simp_idp.hlean.expected.out
@@ -0,0 +1,8 @@
+simp_idp.hlean:7:2: proof state
+A : Type,
+C : A → Type,
+a : A,
+f g : C a → C a,
+c : C a,
+a_1 : f = g
+⊢ f c = g c