added rewrite rules that don't work

mit-plv · Jul 3, 2023 · aed9233 · aed9233
1 parent 628f6a7
commit aed9233
Show file tree

Hide file tree

Showing 5 changed files with 492 additions and 13 deletions.
diff --git a/src/Arithmetic/ADK.v b/src/Arithmetic/ADK.v
@@ -26,3 +26,5 @@ Definition adk_mul_prod_at_i (n : nat) (x y products f : list Z) (i : nat) : Z :
            (fun f => adk_mul' n x y products (rev f))
            (fun p _ g => fun f' => Let_In ((nth' 0%nat f' 0) + p) (fun x => g (x :: f'))) 
            products) [].
+
+  Definition ident_adk_mul := adk_mul.
diff --git a/src/Language/IdentifierParameters.v b/src/Language/IdentifierParameters.v
@@ -194,7 +194,7 @@ Definition all_ident_named_interped : InductiveHList.hlist
       ; with_name ident_fancy_selm ident.fancy.selm
       ; with_name ident_fancy_sell ident.fancy.sell
       ; with_name ident_fancy_addm ident.fancy.addm
-      ; with_name ident_adk_mul adk_mul
+      ; with_name ident_adk_mul ident_adk_mul
      ]%hlist.
 
 Definition scraped_data : ScrapedData.t