From 783678fd18d3b680fc1309ed504bae2c00251b51 Mon Sep 17 00:00:00 2001 From: Ramana Kumar Date: Sun, 20 Oct 2024 13:19:22 +0100 Subject: [PATCH] Avoid double computeLib entry for word_exp also make style even more consistent with word_mul --- src/n-bit/wordsScript.sml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/n-bit/wordsScript.sml b/src/n-bit/wordsScript.sml index f2fc343839..7d17c753b9 100644 --- a/src/n-bit/wordsScript.sml +++ b/src/n-bit/wordsScript.sml @@ -261,6 +261,9 @@ val word_add_def = zDefine` val word_mul_def = zDefine` word_mul (v:'a word) (w:'a word) = (n2w:num->'a word) (w2n v * w2n w)` +val word_exp_def = zDefine` + word_exp (v:'a word) (w:'a word) = (n2w:num->'a word) (w2n v ** w2n w)` + val word_log2_def = zDefine` word_log2 (w:'a word) = (n2w (LOG2 (w2n w)):'a word)` @@ -311,9 +314,6 @@ val word_rem_def = Define` val word_L2_def = Define `word_L2 = word_mul word_L word_L` -val word_exp_def = Define` - word_exp (v:'a word) (w: 'a word) = n2w (w2n v ** w2n w): 'a word` - val () = List.app (fn (s, t) => Parse.overload_on (s, Parse.Term t)) [("+", `$word_add`), ("-", `$word_sub`),