diff options
| author |  jadep <jade.philipoom@gmail.com> | 2016-04-29 15:44:07 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2016-04-29 15:44:07 -0400 |
| commit | f932c72dc669d4ae8e152f6a117a03c25e6dbabd (patch) | |
| tree | 5765e60cd039634ea59b2f9b1f0c3120247ec0ff /src/Spec/ModularWordEncoding.v | |
| parent | a82770a13960d214a76265620096d0f266ca00cd (diff) | |
Moved sign_bit definition to Spec.
Diffstat (limited to 'src/Spec/ModularWordEncoding.v')
| -rw-r--r-- | src/Spec/ModularWordEncoding.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/Spec/ModularWordEncoding.v b/src/Spec/ModularWordEncoding.v index 262b1054d..7772a124c 100644 --- a/src/Spec/ModularWordEncoding.v +++ b/src/Spec/ModularWordEncoding.v @@ -22,6 +22,12 @@ Section ModularWordEncoding. else None . + Definition sign_bit (x : F m) := + match (Fm_enc x) with + | Word.WO => false + | Word.WS b _ w' => b + end. + Instance modular_word_encoding : encoding of F m as word sz := { enc := Fm_enc; dec := Fm_dec; |