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

fix(tests): use have instead of assert

Browse source
This commit is contained in:
Floris van Doorn 2016-03-03 13:00:38 -05:00
parent c50ab524a5
commit ea775092bb
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -69,8 +69,8 @@ theorem lem_eq_iff_vector_inj (A : Type) [inh : inhabited A] : lem_eq A ↔ vect
iff.intro iff.intro
(assume Hl : lem_eq A, (assume Hl : lem_eq A,
assume n m he, assume n m he,
assert a : A, from default A, have a : A, from default A,
assert v : vector A n, from const n a, have v : vector A n, from const n a,
have e₁ : v == cast he v, from heq.symm (cast_heq he v), have e₁ : v == cast he v, from heq.symm (cast_heq he v),
Hl n m v (cast he v) e₁) Hl n m v (cast he v) e₁)
(assume Hr : vector_inj A, (assume Hr : vector_inj A,