From fc4c6454a7f9175fac58c18744b7b2769fd18567 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 17 Jan 2014 14:36:55 -0800
Subject: [PATCH] chore(tests/lean): adjust tests to reflect recent changes

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/builtin/obj/cast.olean         | Bin 1878 -> 2848 bytes
 tests/lean/bug.lean                |   2 +-
 tests/lean/bug.lean.expected.out   |   4 ++--
 tests/lean/eq3.lean                |   7 ++++---
 tests/lean/eq3.lean.expected.out   |   3 ++-
 tests/lean/find.lean.expected.out  |   6 +++---
 tests/lean/tst11.lean.expected.out |   2 +-
 tests/lean/tst4.lean.expected.out  |   2 +-
 8 files changed, 14 insertions(+), 12 deletions(-)

diff --git a/src/builtin/obj/cast.olean b/src/builtin/obj/cast.olean
index 363cd6d3b92a57ae797348d9e8b28a42198c5a13..0b2e2662475a37c7770d36e95b065a01d03510b9 100644
GIT binary patch
literal 2848
zcmZveTXPge6vyYX8A7q~Qie<tR0eW`R9=8Y%225iEv@*1FL?s2)EGBHx!Ekc8%#ce
zJWz%B8I%VK<r~`n-`Sb&9WxJS&*k6e)_uD7xZ5dvhflkmX#B-bkNU@hQS@tP(Cc)g
zvGkxERqT__v*>v_h?0YHIEu35ev~A8XZ_A@<b<!yOO}+;N|HEabRmwC-6(eYSj1sU
zqy*vnqrQImk~l6;&F#K|$TeT!)&+6jl$_|xR+B_f6XZW##j$DH`pHC6krt#1Iqf7D
za`a>zvh4T6koVVwwwkJNcu|#Ro6V9#C!K<8FM$?mRW&+h*EK>qYEML`B<9ZYQ)rPJ
zSu@<s3)3R=1+nvJbF{0XmrMaaqjeXgT@*=00yi1S&Qy68tOQ9vJ{25}Ze7D{jU&?!
zWw)e1^6bZAX90ZT*;%o3Xy?S{R;$<rSn9euoeXb9vDG0PDXds6l2>Y_&#P_ws!jVp
zz&X4fIxN(YY431LiwcoUgzDOu??`T%H{78*IPU#2kkOgt?c&sUpSNgGAw!FrJ{P-<
z7Dp|MOC;L7Ex-;kn+fWkl<4Tmye*OvI2iI|(;=y>t?KxGAR%^NeSjxNW;Z-ttc27@
znI@|;H$<W{ur;w@60OQYtQ~`E;vP`@b+K;blF{*gJ%-Z#AYz@M#Z(HJtm3MJ1tp9I
zWp5ZxVSS%`BZn?mH&7FEgHj~bL>-8W9#%!>zDV0{ilmwJHuaUW3s}f<yovILrG3NI
zNODp|+%bNMjf)Ic9las8b&N2^+RXvrh88@8z3JI?v3YYu{84x;`y)Kk*`OLM%~>GJ
zMPDdK(rOZ(gsl&_Ynq+AJ5eyJtSr2{LQdu><wvn}rV!^n`4lr5?7R`Jkc`W&xXeY{
z45Q&ANWKsXW$sh(<7;I#EQ^igJiM9Vx|{o8lQDya<CS3_hV0QvoeNn31jCCK9EmmO
zc6fGlB>Xsgz(a}P?6mDk4q6MSkn-Hyq1lFQA&W+_D7_=r&?WYyzD$<g(loqF`X}A)
z<Q!Hr#g*(#=e>b!@8t^FKJSfFlEnV3dXVxZ>8uZ0G4Wtx1D|?W%4o&jRy}cY#KlUT
zD$3rLRGjUIKO8LoLl#O}V-Pu&HmRF3{f_nvvG&^C75f71mtxznwD~3Mj<m0u^Gh5e
z{we#~hA0k5b&;jKB*<49^0H6+wN~<C`l_rn8G_kr0+-z}9CQx5f{l-%=B<7>$<8JS
zmPCSU^KUKtOT@N<T_N%tvZHkYNJz8nd4Ku%&xnld6las3eI*_K?0{OyEG=Xr-dl0O
rpPSr|BBp<2hkGaPUy=7BDS>|z>w#Fn)RS;qST_mZ_J00O|BC+u%Icwp

delta 255
zcmZ1=c8zbs^o=u&nJ4$LxH0-ozRJ=%S%XC&oq?4B2$VnsgsBW-`GG}M5KL7NQ=EgT
z*pPuy4aDXK5j-G597F_w2!F7QF^CBk1WPl6WhP%_tzrzE?89cmm@v7MEuJk9B+NAV
z0lVyEZgzRCR1g=eK3xmM%mfiqAVL8|n1Tqfnv}^Q?CPTFAU;?*iy9MCNq&54Ap^tY
c9(GTl9oN_m1muCz%#4hTu6ZeLnK`Kp0Hs<XumAu6

diff --git a/tests/lean/bug.lean b/tests/lean/bug.lean
index a525b9897..7b9c486ce 100644
--- a/tests/lean/bug.lean
+++ b/tests/lean/bug.lean
@@ -1 +1 @@
-check fun (A A' : (Type U')) (H : A = A'), symm H
+check fun (A A' : (Type U)) (H : A = A'), symm H
diff --git a/tests/lean/bug.lean.expected.out b/tests/lean/bug.lean.expected.out
index 8d20643d3..3c39a30a2 100644
--- a/tests/lean/bug.lean.expected.out
+++ b/tests/lean/bug.lean.expected.out
@@ -1,8 +1,8 @@
   Set: pp::colors
   Set: pp::unicode
 Failed to solve
-A : (Type U'), A' : (Type U') ⊢ ?M::4 ≺ (Type U')
-    bug.lean:1:37: Type of argument 1 must be convertible to the expected type in the application of
+A : (Type U), A' : (Type U) ⊢ ?M::4 ≺ (Type U)
+    bug.lean:1:36: Type of argument 1 must be convertible to the expected type in the application of
         @eq
     with arguments:
         ?M::0
diff --git a/tests/lean/eq3.lean b/tests/lean/eq3.lean
index 01999f540..a8c4741ae 100644
--- a/tests/lean/eq3.lean
+++ b/tests/lean/eq3.lean
@@ -1,8 +1,9 @@
+import heq
 variable Vector : Nat -> Type
 variable n  : Nat
 variable v1 : Vector n
 variable v2 : Vector (n + 0)
 variable v3 : Vector (0 + n)
-axiom cast {A B : TypeU} : A = B -> A -> B
-axiom H1 : v1 = cast (congr2 Vector (Nat::add_zeror n)) v2
-axiom H2 : v2 = cast (congr2 Vector (Nat::add_comm 0 n)) v3
+axiom H1 : v1 == v2
+axiom H2 : v2 == v3
+check htrans H1 H2
diff --git a/tests/lean/eq3.lean.expected.out b/tests/lean/eq3.lean.expected.out
index 211df19f5..871de95c3 100644
--- a/tests/lean/eq3.lean.expected.out
+++ b/tests/lean/eq3.lean.expected.out
@@ -1,10 +1,11 @@
   Set: pp::colors
   Set: pp::unicode
+  Imported 'heq'
   Assumed: Vector
   Assumed: n
   Assumed: v1
   Assumed: v2
   Assumed: v3
-  Assumed: cast
   Assumed: H1
   Assumed: H2
+htrans H1 H2 : v1 == v3
diff --git a/tests/lean/find.lean.expected.out b/tests/lean/find.lean.expected.out
index 466f89f5c..e403cbf09 100644
--- a/tests/lean/find.lean.expected.out
+++ b/tests/lean/find.lean.expected.out
@@ -1,8 +1,8 @@
   Set: pp::colors
   Set: pp::unicode
   Imported 'find'
-theorem congr1 {A : TypeU'} {B : A → TypeU'} {f g : ∀ x : A, B x} (a : A) (H : f = g) : f a = g a
-theorem congr2 {A B : TypeU'} {a b : A} (f : A → B) (H : a = b) : f a = f b
-theorem congr {A B : TypeU'} {f g : A → B} {a b : A} (H1 : f = g) (H2 : a = b) : f a = g b
+theorem congr1 {A : TypeU} {B : A → TypeU} {f g : ∀ x : A, B x} (a : A) (H : f = g) : f a = g a
+theorem congr2 {A B : TypeU} {a b : A} (f : A → B) (H : a = b) : f a = f b
+theorem congr {A B : TypeU} {f g : A → B} {a b : A} (H1 : f = g) (H2 : a = b) : f a = g b
 find.lean:3:0: error: executing external script (/home/leo/projects/lean/build/debug/shell/find.lua:24), no object name in the environment matches the regular expression 'foo'
 find.lean:4:0: error: executing external script (/home/leo/projects/lean/build/debug/shell/find.lua:18), unfinished capture
diff --git a/tests/lean/tst11.lean.expected.out b/tests/lean/tst11.lean.expected.out
index 9830b2040..02af3b075 100644
--- a/tests/lean/tst11.lean.expected.out
+++ b/tests/lean/tst11.lean.expected.out
@@ -6,7 +6,7 @@
 ⊤
   Assumed: a
 a ⊕ a ⊕ a
-@subst : ∀ (A : TypeU') (a b : A) (P : A → Bool), P a → a = b → P b
+@subst : ∀ (A : TypeU) (a b : A) (P : A → Bool), P a → a = b → P b
   Proved: EM2
 EM2 : ∀ a : Bool, a ∨ ¬ a
 EM2 a : a ∨ ¬ a
diff --git a/tests/lean/tst4.lean.expected.out b/tests/lean/tst4.lean.expected.out
index 71a1b8a37..6201629bc 100644
--- a/tests/lean/tst4.lean.expected.out
+++ b/tests/lean/tst4.lean.expected.out
@@ -10,7 +10,7 @@
   Assumed: EqNice
 @EqNice N n1 n2
 @f N n1 n2 : N
-@congr : ∀ (A B : TypeU') (f g : A → B) (a b : A), @eq (A → B) f g → @eq A a b → @eq B (f a) (g b)
+@congr : ∀ (A B : TypeU) (f g : A → B) (a b : A), @eq (A → B) f g → @eq A a b → @eq B (f a) (g b)
 @f N n1 n2
   Assumed: a
   Assumed: b