From bb8a935f9143e65102a3a498a96dd13a3b8a4801 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Sun, 24 May 2020 13:36:53 +0100
Subject: Add HTLgen

---
 src/verilog/AssocMap.v | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

(limited to 'src/verilog/AssocMap.v')

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.
 
-- 
cgit