From 1d6589fbda24fb57c9ab74d4bd41fa1a487a2c62 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Thu, 7 May 2020 17:21:37 +0100 Subject: Remove Admitted Maps Lemma --- src/common/Maps.v | 6 ------ 1 file changed, 6 deletions(-) (limited to 'src') 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. -- cgit