diff options
| author | Nickolai Zeldovich | 2014-11-09 11:55:00 -0500 |
|---|---|---|
| committer | Pierre Letouzey | 2015-04-09 12:33:51 +0200 |
| commit | 30446765297d79767b68e4a5f5b9160171b63b72 (patch) | |
| tree | 56b998c575dc3ea72171b93652b718a4b4e00500 /kernel/cbytecodes.mli | |
| parent | 1688d4af1896effb42fa5dd191948795c59288a4 (diff) | |
Add a [map_ext_in] lemma to List.v.
Slightly broader version of the existing [map_ext]: two [map] expressions
are equal if their respective functions agree on all arguments that are
in the list being mapped.
Diffstat (limited to 'kernel/cbytecodes.mli')
0 files changed, 0 insertions, 0 deletions