diff options
Diffstat (limited to 'riscv/prelude.sail')
| -rw-r--r-- | riscv/prelude.sail | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/riscv/prelude.sail b/riscv/prelude.sail index 89221596..b58ebc52 100644 --- a/riscv/prelude.sail +++ b/riscv/prelude.sail @@ -1,7 +1,7 @@ default Order dec type bits ('n : Int) = vector('n, dec, bit) -union option ('a : Type) = {None, Some : 'a} +union option ('a : Type) = {None : unit, Some : 'a} val eq_atom = {ocaml: "eq_int", lem: "eq"} : forall 'n 'm. (atom('n), atom('m)) -> bool val lteq_atom = "lteq" : forall 'n 'm. (atom('n), atom('m)) -> bool @@ -330,9 +330,9 @@ val print_string = "print_string" : (string, string) -> unit union exception = { Error_not_implemented : string, - Error_misaligned_access, - Error_EBREAK, - Error_internal_error + Error_misaligned_access : unit, + Error_EBREAK : unit, + Error_internal_error : unit } val "sign_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m) |