diff options
Diffstat (limited to 'mips/mips_extras.v')
| -rw-r--r-- | mips/mips_extras.v | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/mips/mips_extras.v b/mips/mips_extras.v index 94e4779c..49899107 100644 --- a/mips/mips_extras.v +++ b/mips/mips_extras.v @@ -152,3 +152,11 @@ Qed. Definition mults_vec {n} (l : mword n) (r : mword n) : mword (2 * n) := mults_vec l r. Definition mult_vec {n} (l : mword n) (r : mword n) : mword (2 * n) := mult_vec l r. + + +Definition print_endline (_:string) : unit := tt. +Definition prerr_endline (_:string) : unit := tt. +Definition prerr_string (_:string) : unit := tt. +Definition putchar {T} (_:T) : unit := tt. +Require DecimalString. +Definition string_of_int z := DecimalString.NilZero.string_of_int (Z.to_int z). |