diff options
Diffstat (limited to 'src/verilog/AssocMap.v')
| -rw-r--r-- | src/verilog/AssocMap.v | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/src/verilog/AssocMap.v b/src/verilog/AssocMap.v index 9caa2d1..cac2c02 100644 --- a/src/verilog/AssocMap.v +++ b/src/verilog/AssocMap.v @@ -43,15 +43,14 @@ Module AssocMapExt. forall am am' r v, merge (add r v am) am' = add r v (merge am am'). Proof. - intros. - unfold merge. - Search fold_right. - apply SetoidList.fold_right_add2. + induction am; intros. + unfold merge. simpl. unfold fold_right. simpl. Search MapsTo. + Abort. Lemma merge_base : forall am, merge (empty elt) am = am. - Proof. intros. unfold merge. apply fold_1. Qed. + Proof. auto. Qed. End Operations. |