diff options
| author | Brian Campbell | 2018-06-07 18:00:59 +0100 |
|---|---|---|
| committer | Brian Campbell | 2018-06-08 15:03:37 +0100 |
| commit | 7cdbee76d454047271ef6cdaa82a2b7e2ed590ba (patch) | |
| tree | c0f6e3843758e009551c9de53afbe227ed3df31f /lib | |
| parent | dda8dd8689ea4756c41a5bb36a123b564dfb0b12 (diff) | |
Coq: add destructuring of atom existentials in patterns
Plus test case, broken builtin name
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/vector_dec.sail | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/vector_dec.sail b/lib/vector_dec.sail index 60f49af8..d9b80b32 100644 --- a/lib/vector_dec.sail +++ b/lib/vector_dec.sail @@ -122,7 +122,7 @@ val unsigned = { lem: "uint", interpreter: "uint", c: "sail_uint", - coq: "uint" + coq: "unsigned" } : forall 'n. bits('n) -> range(0, 2 ^ 'n - 1) val signed = "sint" : forall 'n. bits('n) -> range(- (2 ^ ('n - 1)), 2 ^ ('n - 1) - 1) |