From d43e0891ae47457dd1d2682e3fbdf6328ad84130 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 16 Jun 2015 13:01:24 -0700
Subject: [PATCH] fix(library/init/logic): make sure library can be compiled
 using '--to_axiom' option

---
 library/data/vector.lean | 4 ++--
 library/init/logic.lean  | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/library/data/vector.lean b/library/data/vector.lean
index 85a92502b..d37774b74 100644
--- a/library/data/vector.lean
+++ b/library/data/vector.lean
@@ -77,7 +77,7 @@ namespace vector
 
   theorem nth_tabulate : ∀ {n : nat} (f : fin n → A) (i : fin n), nth (tabulate f) i = f i
   | 0     f i               := elim0 i
-  | (n+1) f (mk 0 h)        := rfl
+  | (n+1) f (mk 0 h)        := by reflexivity
   | (n+1) f (mk (succ i) h) :=
     begin
       change nth (f (@zero n) :: tabulate (λ i : fin n, f (succ i))) (mk (succ i) h) = f (mk (succ i) h),
@@ -97,7 +97,7 @@ namespace vector
 
   theorem nth_map (f : A → B) : ∀ {n : nat} (v : vector A n) (i : fin n), nth (map f v) i = f (nth v i)
   | 0        v        i               := elim0 i
-  | (succ n) (a :: t) (mk 0 h)        := rfl
+  | (succ n) (a :: t) (mk 0 h)        := by reflexivity
   | (succ n) (a :: t) (mk (succ i) h) := by rewrite [map_cons, *nth_succ, nth_map]
 
   definition map2 (f : A → B → C) : Π {n : nat}, vector A n → vector B n → vector C n
diff --git a/library/init/logic.lean b/library/init/logic.lean
index a4275a13c..9f7c4f10c 100644
--- a/library/init/logic.lean
+++ b/library/init/logic.lean
@@ -34,7 +34,7 @@ assume Hna : ¬a, absurd Ha Hna
 /- eq -/
 
 notation a = b := eq a b
-theorem rfl {A : Type} {a : A} : a = a := eq.refl a
+definition rfl {A : Type} {a : A} : a = a := eq.refl a
 
 -- proof irrelevance is built in
 theorem proof_irrel {a : Prop} (H₁ H₂ : a) : H₁ = H₂ :=