diff options
Diffstat (limited to 'src/Spec/ModularWordEncoding.v')
| -rw-r--r-- | src/Spec/ModularWordEncoding.v | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/src/Spec/ModularWordEncoding.v b/src/Spec/ModularWordEncoding.v index 9f7e3340b..262b1054d 100644 --- a/src/Spec/ModularWordEncoding.v +++ b/src/Spec/ModularWordEncoding.v @@ -25,7 +25,10 @@ Section ModularWordEncoding. Instance modular_word_encoding : encoding of F m as word sz := { enc := Fm_enc; dec := Fm_dec; - encoding_valid := @ModularWordEncodingPre.Fm_encoding_valid m sz m_pos bound_check + encoding_valid := + @ModularWordEncodingPre.Fm_encoding_valid m sz m_pos bound_check; + encoding_canonical := + @ModularWordEncodingPre.Fm_encoding_canonical m sz bound_check }. End ModularWordEncoding. |