Revision 7a7a1aa403201894461c5ff40ae9fee67be399f3 authored by Raphaël Cauderlier on 31 May 2021, 22:11:03 UTC, committed by Raphaël Cauderlier on 31 May 2021, 22:11:03 UTC
Before this commit, set.remove uses List.remove which only computes when its decide_equality argument does. We passed it an opaque lemma so it did not compute. Moreover, it always scanned the whole list but since we only apply it on sorted lists it could stop as soon as it encounters a value larger than the one to remove. This commit redefines set.remove so that it does not depend on decidability of equality anymore and returns as soon as it can.
1 parent 6406bf3
File | Mode | Size |
---|---|---|
talk_01_14_2020_visit_cobra | ||
talk_08_09_2019_coq_workshop | ||
talk_11_10_2019_FMBC_workshop | ||
talk_12_03_2019_multisig_lightling_talk | ||
talk_14_02-2020_WTSC | ||
talk_15_10_2019_ledger_meetup | ||
talk_17_09_2018_interview | ||
talk_20_05_2019_irif_semverif | ||
talk_27_06_2019_chainacc_training | ||
talk_30_01_2020_deducteam_seminar | ||
LogoNL.jpg | -rw-r--r-- | 162.7 KB |
logo_albert.png | -rw-r--r-- | 2.9 KB |
logo_michocoq.png | -rw-r--r-- | 30.1 KB |
logo_pile_qui_chante.png | -rw-r--r-- | 85.8 KB |
logo_tezos.tikz | -rw-r--r-- | 1.8 KB |
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...