feat(hott/init/path): mark 'idp' and 'idpath' with '[unfold-m]' hint

closes #496

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}

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

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