diff options
| author | James Pollard <james@pollard.dev> | 2020-06-09 16:03:22 +0100 |
|---|---|---|
| committer | James Pollard <james@pollard.dev> | 2020-06-09 16:03:22 +0100 |
| commit | 7971f2f570de84204aeca2cb72001dc3e824501d (patch) | |
| tree | da10753bc6563944309bd23b4dff41185a3e9e43 /src/verilog/AssocMap.v | |
| parent | 6426456c4cc7c6d11cf0204ff3d3c0aa18762323 (diff) | |
| parent | 86e1d027bb556e0e1f5a39c93b41130603f4f9ad (diff) | |
| download | vericert-7971f2f570de84204aeca2cb72001dc3e824501d.tar.gz vericert-7971f2f570de84204aeca2cb72001dc3e824501d.zip | |
Merge branch 'develop' into arrays-proof
Diffstat (limited to 'src/verilog/AssocMap.v')
| -rw-r--r-- | src/verilog/AssocMap.v | 19 |
1 files changed, 13 insertions, 6 deletions
diff --git a/src/verilog/AssocMap.v b/src/verilog/AssocMap.v index 88b13a6..5d531d5 100644 --- a/src/verilog/AssocMap.v +++ b/src/verilog/AssocMap.v @@ -202,9 +202,16 @@ Ltac unfold_merge := unfold merge_assocmap; try (repeat (rewrite merge_add_assoc)); rewrite AssocMapExt.merge_base_1. -Module AssocMapNotation. - Notation "a ! b" := (AssocMap.get b a) (at level 1). - Notation "a # ( b , c )" := (find_assocmap c b a) (at level 1). - Notation "a # b" := (find_assocmap 32 b a) (at level 1). - Notation "a ## b" := (List.map (fun c => find_assocmap 32 c a) b) (at level 1). -End AssocMapNotation. +Declare Scope assocmap. +Notation "a ! b" := (AssocMap.get b a) (at level 1) : assocmap. +Notation "a # ( b , c )" := (find_assocmap c b a) (at level 1) : assocmap. +Notation "a # b" := (find_assocmap 32 b a) (at level 1) : assocmap. +Notation "a ## b" := (List.map (fun c => find_assocmap 32 c a) b) (at level 1) : assocmap. +Notation "a # b '<-' c" := (AssocMap.set b c a) (at level 1, b at next level) : assocmap. + +Local Open Scope assocmap. +Lemma find_get_assocmap : + forall assoc r v, + assoc ! r = Some v -> + assoc # r = v. +Proof. intros. unfold find_assocmap, AssocMapExt.get_default. rewrite H. trivial. Qed. |