diff options
| author | Brian Campbell | 2018-07-17 13:19:53 +0100 |
|---|---|---|
| committer | Brian Campbell | 2018-07-17 13:19:53 +0100 |
| commit | 48cc76254b6cbbf536a0424275087b084d40f4cb (patch) | |
| tree | c31d5127839d6c9468ad8fe48d281fe4aec4633f /lib | |
| parent | 48c73e33a621034ba020b9b1bc83c5f70a19314f (diff) | |
Coq: add printing stubs
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/coq/Sail2_values.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v index 0bd4707d..63cf7542 100644 --- a/lib/coq/Sail2_values.v +++ b/lib/coq/Sail2_values.v @@ -112,7 +112,12 @@ Definition negate_real r := realNegate r Definition abs_real r := realAbs r Definition power_real b e := realPowInteger b e*) +Definition print_endline (_ : string) : unit := tt. +Definition prerr_endline (_ : string) : unit := tt. +Definition prerr (_ : string) : unit := tt. Definition print_int (_ : string) (_ : Z) : unit := tt. +Definition prerr_int (_ : string) (_ : Z) : unit := tt. +Definition putchar (_ : Z) : unit := tt. (* Definition or_bool l r := (l || r) |