mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
3671864507
- New examples using the new syntax (+=, ...) - New examples using the new methods (.pop(), .append(), ...) - Update old examples with assignement operators (+=, ...)
9 lines
235 B
Python
9 lines
235 B
Python
def check_duplicates(elt, tab):
|
|
#@ ensures result == occurrence(elt, tab, 0, len(tab))
|
|
nb = 0
|
|
for e in tab:
|
|
#@ invariant nb == occurrence(elt, tab, 0, e'index)
|
|
if e == elt:
|
|
nb += 1
|
|
return nb
|