diff options
Diffstat (limited to 'test/mono/test_extra.lem')
| -rw-r--r-- | test/mono/test_extra.lem | 9 |
1 files changed, 3 insertions, 6 deletions
diff --git a/test/mono/test_extra.lem b/test/mono/test_extra.lem index a567257c..9c526309 100644 --- a/test/mono/test_extra.lem +++ b/test/mono/test_extra.lem @@ -5,12 +5,9 @@ open import Sail_operators_mwords open import Prompt_monad open import State -let undefined_int () = (0:ii) -val undefined_bitvector : forall 'a. Size 'a => integer -> mword 'a -let undefined_bitvector len = duplicate B0 len - -val uint : forall 'a. Size 'a => mword 'a -> integer -let uint = unsigned +let undefined_int () = return (0:ii) +val undefined_bitvector : forall 'rv 'a 'e. Bitvector 'a => integer -> monad 'rv 'a 'e +let undefined_bitvector len = return (of_bools (repeat [false] len)) val slice : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> integer -> mword 'b let slice v lo len = |