diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-05-07 17:21:37 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-05-07 17:21:37 +0100 |
| commit | 1d6589fbda24fb57c9ab74d4bd41fa1a487a2c62 (patch) | |
| tree | 7922e64d394da02183738ba959003fa8ef5f7d2a /src/common | |
| parent | 74ac24f8dc099cc558d3b03b2f9303c89048f519 (diff) | |
| download | vericert-1d6589fbda24fb57c9ab74d4bd41fa1a487a2c62.tar.gz vericert-1d6589fbda24fb57c9ab74d4bd41fa1a487a2c62.zip | |
Remove Admitted Maps Lemma
Diffstat (limited to 'src/common')
| -rw-r--r-- | src/common/Maps.v | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/src/common/Maps.v b/src/common/Maps.v index 7a542b7..3236417 100644 --- a/src/common/Maps.v +++ b/src/common/Maps.v @@ -40,10 +40,4 @@ Definition traverse (A B : Type) (f : positive -> A -> res B) m := xtraverse f m Definition traverse1 (A B : Type) (f : A -> res B) := traverse (fun _ => f). -Lemma traverse1_inversion: - forall (A B : Type) (f : A -> res B) (i j : positive) (m : t A) (m' : t B), - traverse1 f m = OK m' -> - list_forall2 (fun x y => f (snd x) = OK (snd y) /\ fst x = fst y) (elements m) (elements m'). -Proof. Admitted. - End PTree. |