From 502e49e2f8c95b40cd0761cbb69c863904169f8b Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sat, 29 Jul 2023 13:49:03 +0100 Subject: Add beginning to memory generation proof --- src/hls/AssocMap.v | 1 + 1 file changed, 1 insertion(+) (limited to 'src/hls/AssocMap.v') diff --git a/src/hls/AssocMap.v b/src/hls/AssocMap.v index ee39e8e..0c9242c 100644 --- a/src/hls/AssocMap.v +++ b/src/hls/AssocMap.v @@ -243,6 +243,7 @@ Ltac unfold_merge := rewrite AssocMapExt.merge_base_1. 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. -- cgit