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 standard library

Browse source
This commit is contained in:
Leonardo de Moura 2015-06-10 17:00:47 -07:00
parent 226a5800dd
commit 8aa634378e
3 changed files with 6 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
tests/lean/rateval.lean.expected.out
View file

@ -1 +1 @@
quot.mk (prerat.mk 14 6 (mul_denom_pos (prerat.mul (prerat.of_int 8) (prerat.inv (prerat.of_int 6))) prerat.one))
quot.mk (prerat.mk 14 6 (mul_denom_pos (prerat.mul (prerat.of_int 8) (prerat.inv (prerat.of_int 6))) (prerat.of_int 1)))

6
tests/lean/run/new_obtain3.lean
View file

@ -8,8 +8,8 @@ setext (take z,
iff.intro
(assume Hz : z ∈ (f ∘ g) '[a],
obtain x (Hx₁ : x ∈ a) (Hx₂ : f (g x) = z), from Hz,
have Hgx : g x ∈ g '[a], from in_image Hx₁ rfl,
show z ∈ f '[g '[a]], from in_image Hgx Hx₂)
have Hgx : g x ∈ g '[a], from mem_image Hx₁ rfl,
show z ∈ f '[g '[a]], from mem_image Hgx Hx₂)
(assume Hz : z ∈ f '[g '[a]],
obtain y [x (Hz₁ : x ∈ a) (Hz₂ : g x = y)] (Hy₂ : f y = z), from Hz,
show z ∈ (f ∘ g) '[a], from in_image Hz₁ (Hz₂⁻¹ ▸ Hy₂)))
show z ∈ (f ∘ g) '[a], from mem_image Hz₁ (Hz₂⁻¹ ▸ Hy₂)))

4
tests/lean/run/new_obtain4.lean
View file

@ -8,7 +8,7 @@ setext (take z,
iff.intro
(assume Hz,
obtain x Hx₁ Hx₂, from Hz,
by repeat (apply in_image | assumption | reflexivity))
by repeat (apply mem_image | assumption | reflexivity))
(assume Hz,
obtain y [x Hz₁ Hz₂] Hy₂, from Hz,
by repeat (apply in_image | assumption | esimp [compose] | rewrite Hz₂)))
by repeat (apply mem_image | assumption | esimp [compose] | rewrite Hz₂)))