Skip to content

Commit

Permalink
remove unproven Map theorem
Browse files Browse the repository at this point in the history
  • Loading branch information
jyluo committed Apr 9, 2018
1 parent ac41fbf commit 04397e8
Showing 1 changed file with 0 additions and 13 deletions.
13 changes: 0 additions & 13 deletions coq-proof/MapsDefs.v
Original file line number Diff line number Diff line change
Expand Up @@ -47,19 +47,6 @@ Proof.
rewrite H in H0. apply H0.
Qed.

(*
Theorem Map_Add_Eq :
forall {K V : Type} (key_eq : K -> K -> bool) (m : Map K V) (k : K) (v : V),
Map_Get key_eq (Map_Add key_eq m k v) k = Some v.
Proof.
intros.
unfold Map_Get. unfold Map_Add.
induction m; subst.
destruct (key_eq_dec key_eq k k).
rewrite -> e. reflexivity.
Qed.
*)

Definition Map_Contains {K V : Type} (key_eq : K -> K -> bool) (m : Map K V) (k : K) : bool :=
match Map_Get key_eq m k with
| None => false
Expand Down

0 comments on commit 04397e8

Please sign in to comment.