Coq: add some string functions

1 files changed, 3 insertions, 2 deletions

diff --git a/lib/coq/Sail2_operators_mwords.v b/lib/coq/Sail2_operators_mwords.v
index ee98c94e..bb4bf053 100644
--- a/lib/coq/Sail2_operators_mwords.v
+++ b/lib/coq/Sail2_operators_mwords.v
@@ -3,6 +3,7 @@ Require Import Sail2_operators.
 Require Import Sail2_prompt_monad.
 Require Import Sail2_prompt.
 Require Import bbv.Word.
+Require bbv.BinNotation.
 Require Import Arith.
 Require Import ZArith.
 Require Import Omega.
@@ -267,8 +268,8 @@ Definition msb := most_significant
 val int_of_vec : forall 'a. Size 'a => bool -> mword 'a -> integer
 Definition int_of_vec := int_of_bv
 
-val string_of_vec : forall 'a. Size 'a => mword 'a -> string
-Definition string_of_vec := string_of_bv*)
+val string_of_vec : forall 'a. Size 'a => mword 'a -> string*)
+Definition string_of_bits {n} (w : mword n) : string := string_of_bv w.
 Definition with_word' {n} (P : Type -> Type) : (forall n, Word.word n -> P (Word.word n)) -> mword n -> P (mword n) := fun f w => @with_word n _ (f (Z.to_nat n)) w.
 Definition word_binop {n} (f : forall n, Word.word n -> Word.word n -> Word.word n) : mword n -> mword n -> mword n := with_word' (fun x => x -> x) f.
 Definition word_unop {n} (f : forall n, Word.word n -> Word.word n) : mword n -> mword n := with_word' (fun x => x) f.