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

chore(tests/lean/extra): fix test

Browse source
This commit is contained in:
Leonardo de Moura 2016-06-02 11:26:53 -07:00
parent 273753f3fc
commit b58eac5013
1 changed files with 2 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
tests/lean/extra/bag.661.20.expected.out
View file

@ -2,15 +2,13 @@ LEAN_INFORMATION
position 661:20
A : Type,
decA : decidable_eq A,
all_of_subcount_eq_tt :
∀ {l₁ l₂ : list A},
subcount l₁ l₂ = tt → (∀ (a : A), list.count a l₁ ≤ list.count a l₂),
all_of_subcount_eq_tt : ∀ {l₁ l₂}, subcount l₁ l₂ = tt → (∀ a, list.count a l₁ ≤ list.count a l₂),
a : A,
l₁ l₂ : list A,
h : subcount (a :: l₁) l₂ = tt,
x : A,
this : subcount l₁ l₂ = tt,
ih : ∀ (a : A), list.count a l₁ ≤ list.count a l₂,
ih : ∀ a, list.count a l₁ ≤ list.count a l₂,
i : list.count a (a :: l₁) ≤ list.count a l₂,
this : x = a
⊢ list.count x (a :: l₁) ≤ list.count x l₂