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

fix(tests/lean): adjust tests to reflect changes in the elaboration process

Browse source
This commit is contained in:
Leonardo de Moura 2015-06-26 17:10:18 -07:00
parent de90926eed
commit 2aa64034df
5 changed files with 4 additions and 21 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
tests/lean/531.hlean
View file

@ -134,18 +134,4 @@ parameters {TL BL TR : Type.{u}} (f : TL → BL) (g : TL → TR)
} }
end end
example
{P : pushout → Type}
{Pinl : Π (x : BL), P (inl x)}
{Pinr : Π (x : TR), P (inr x)}
{Pglue : Π (x : TL), eq (transport (λ (x : pushout), P x) (glue x) (Pinl (f x))) (Pinr (g x))}
{y : pushout}
{x : @ob _ (@dom _ tt)}
: eq (transport (λ (x : pushout), P x) (inverse (coherence x)) (transport P (@cglue _ tt x) (Pinr (g x))))
(Pinl (f x)) :=
begin
rewrite -{(transport (λ (x : pushout), P x) (inverse (coherence x)) (transport P (@cglue _ tt x) (Pinr (g x))))}con_tr,
apply sorry
end
exit exit

2
tests/lean/531.hlean.expected.out
View file

@ -1 +1 @@
531.hlean:151:0: warning: using 'exit' to interrupt Lean 531.hlean:137:0: warning: using 'exit' to interrupt Lean

4
tests/lean/hott/329.hlean
View file

@ -7,9 +7,7 @@ definition path_sigma_dpair (p : a = a') (q : p ▸ b = b') : sigma.mk a b = sig
eq.rec_on p (λb b' q, eq.rec_on q idp) b b' q eq.rec_on p (λb b' q, eq.rec_on q idp) b b' q
definition path_sigma (p : pr1 u = pr1 v) (q : p ▸ pr2 u = pr2 v) : u = v := definition path_sigma (p : pr1 u = pr1 v) (q : p ▸ pr2 u = pr2 v) : u = v :=
destruct u begin cases u, cases v, apply path_sigma_dpair p q end
(λu1 u2, destruct v (λ v1 v2, path_sigma_dpair))
p q
definition path_path_sigma_lemma' {p1 : a = a'} {p2 : p1 ▸ b = b'} {q2 : p1 ▸ b = b'} definition path_path_sigma_lemma' {p1 : a = a'} {p2 : p1 ▸ b = b'} {q2 : p1 ▸ b = b'}
(s : idp ▸ p2 = q2) : path_sigma p1 p2 = path_sigma p1 q2 := (s : idp ▸ p2 = q2) : path_sigma p1 p2 = path_sigma p1 q2 :=

2
tests/lean/hott/615.hlean
View file

@ -16,5 +16,5 @@ protected definition my_decode {x : circle} : my_code x → base = x :=
induction x, induction x,
{ exact power loop}, { exact power loop},
{ apply arrow_pathover_left, intro b, apply concato_eq, apply pathover_eq_r, { apply arrow_pathover_left, intro b, apply concato_eq, apply pathover_eq_r,
rewrite [power_con,transport_code_loop]}, xrewrite [power_con, transport_code_loop]},
end end

3
tests/lean/run/nested_rec.lean
View file

@ -29,8 +29,7 @@ theorem g_succ (a : nat) : g (succ a) = g (g a) :=
have aux : well_founded.fix g.F (succ a) = sigma.mk (g (g a)) _, from have aux : well_founded.fix g.F (succ a) = sigma.mk (g (g a)) _, from
well_founded.fix_eq g.F (succ a), well_founded.fix_eq g.F (succ a),
calc g (succ a) = pr₁ (well_founded.fix g.F (succ a)) : rfl calc g (succ a) = pr₁ (well_founded.fix g.F (succ a)) : rfl
... = pr₁ (sigma.mk (g (g a)) _) : {aux} ... = g (g a) : {aux}
... = g (g a) : rfl
theorem g_all_zero (a : nat) : g a = zero := theorem g_all_zero (a : nat) : g a = zero :=
nat.induction_on a nat.induction_on a