diff options
| author | Cyril Cohen | 2020-11-17 22:45:49 +0100 |
|---|---|---|
| committer | Cyril Cohen | 2020-11-18 01:33:41 +0100 |
| commit | 8eb486ad82accfb1417be11ecc2889aa09c22081 (patch) | |
| tree | b780572ba74f5d464d7adb440de6c9c66f628625 /mathcomp/character/Make | |
| parent | 068284d23c4a05c7ffeb4db8e277d24ed561369f (diff) | |
Adding size_merge_sort_push
This documents the fact that `merge_sort_push` preserves an invariant on its second argument.
Importing a statement and proof by Georges Gonthier, inspired by one of Karl Palmskog's contribution.
Co-Authored-By: Karl Palmskog <palmskog@kth.se>
Co-Authored-By: Georges Gonthier <georges.gonthier@inria.fr>
Diffstat (limited to 'mathcomp/character/Make')
0 files changed, 0 insertions, 0 deletions