michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(tests/lean/run/univ_bug2): old test

Browse source
This commit is contained in:
Leonardo de Moura 2015-10-27 15:54:47 -07:00
parent 6465b16951
commit 54c5d2ca99
1 changed files with 0 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
tests/lean/run/univ_bug2.lean
View file

@ -16,17 +16,8 @@ namespace simplifies_to
theorem get_eq {T : Type} {t1 t2 : T} (C : simplifies_to t1 t2) : t1 = t2 := theorem get_eq {T : Type} {t1 t2 : T} (C : simplifies_to t1 t2) : t1 = t2 :=
simplifies_to.rec (λx, x) C simplifies_to.rec (λx, x) C
theorem infer_eq {T : Type} (t1 t2 : T) [C : simplifies_to t1 t2] : t1 = t2 :=
simplifies_to.rec (λx, x) C
theorem simp_app [instance] (S : Type) (T : Type) (f1 f2 : S → T) (s1 s2 : S) theorem simp_app [instance] (S : Type) (T : Type) (f1 f2 : S → T) (s1 s2 : S)
[C1 : simplifies_to f1 f2] [C2 : simplifies_to s1 s2] : simplifies_to (f1 s1) (f2 s2) := [C1 : simplifies_to f1 f2] [C2 : simplifies_to s1 s2] : simplifies_to (f1 s1) (f2 s2) :=
mk (congr (get_eq C1) (get_eq C2)) mk (congr (get_eq C1) (get_eq C2))
theorem test1 (S : Type) (T : Type) (f1 f2 : S → T) (s1 s2 : S) (Hf : f1 = f2) (Hs : s1 = s2) :
f1 s1 = f2 s2 :=
have Rs [visible] : simplifies_to f1 f2, from mk Hf,
have Cs [visible] : simplifies_to s1 s2, from mk Hs,
infer_eq _ _
end simplifies_to end simplifies_to