diff options
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. |