diff options
| author | Thomas Bauereiss | 2018-03-21 10:35:06 +0000 |
|---|---|---|
| committer | Thomas Bauereiss | 2018-03-21 10:35:06 +0000 |
| commit | e5fc89d249682f8323f987a8275d25403762f658 (patch) | |
| tree | 7107bda5dfbdfa5159e2d55b8a6123c2312ab65c /mips/prelude.sail | |
| parent | b42d5ab44307da291aac1882f8a2bb7bcbdfa900 (diff) | |
Fix Lem generation for MIPS
Diffstat (limited to 'mips/prelude.sail')
| -rw-r--r-- | mips/prelude.sail | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/mips/prelude.sail b/mips/prelude.sail index 63fed9c4..05e4cfe0 100644 --- a/mips/prelude.sail +++ b/mips/prelude.sail @@ -311,8 +311,8 @@ union exception = { Error_internal_error : unit } -val _sign_extend = "sign_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m) -val _zero_extend = "zero_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m) +val _sign_extend = {ocaml: "sign_extend", lem: "_sign_extend"} : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m) +val _zero_extend = {ocaml: "zero_extend", lem: "_zero_extend"} : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m) val sign_extend : forall 'n 'm , 'm >= 'n . bits('n) -> bits('m) val zero_extend : forall 'n 'm , 'm >= 'n . bits('n) -> bits('m) |