Skip to content

Commit

Permalink
Avoid double computeLib entry for word_exp
Browse files Browse the repository at this point in the history
also make style even more consistent with word_mul
  • Loading branch information
xrchz committed Oct 22, 2024
1 parent 3b47d89 commit 783678f
Showing 1 changed file with 3 additions and 3 deletions.
6 changes: 3 additions & 3 deletions src/n-bit/wordsScript.sml
Original file line number Diff line number Diff line change
Expand Up @@ -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)`

Expand Down Expand Up @@ -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`),
Expand Down

0 comments on commit 783678f

Please sign in to comment.