diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/arith.sail | 4 | ||||
| -rw-r--r-- | lib/option.sail | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/lib/arith.sail b/lib/arith.sail index db011f14..a3a80fc5 100644 --- a/lib/arith.sail +++ b/lib/arith.sail @@ -58,13 +58,13 @@ let elsize = shl_int(8, UInt(size)) THIS ensures that in this case the typechecker knows that the end result will be a value in the set `{8, 16, 32, 64}` */ val _shl8 = {c: "shl_mach_int", _: "shl_int"} : - forall 'n, 0 <= 'n <= 3. (int(8), int('n)) -> int('m) with 'm in {8, 16, 32, 64} + forall 'n, 0 <= 'n <= 3. (int(8), int('n)) -> {'m, 'm in {8, 16, 32, 64}. int('m)} /*! Similarly, we can shift 32 by either 0 or 1 to get a value in `{32, 64}` */ val _shl32 = {c: "shl_mach_int", _: "shl_int"} : - forall 'n, 'n in {0, 1}. (int(32), int('n)) -> int('m) with 'm in {32, 64} + forall 'n, 'n in {0, 1}. (int(32), int('n)) -> {'m, 'm in {32, 64}. int('m)} val _shl_int = "shl_int" : (int, int) -> int diff --git a/lib/option.sail b/lib/option.sail index 3869167b..514cf7ba 100644 --- a/lib/option.sail +++ b/lib/option.sail @@ -6,7 +6,7 @@ $define _OPTION // this won't work - also no other type should be created with // constructors named Some or None. -union option ('a : Type) = { +union option('a: Type) = { Some : 'a, None : unit } |