diff options
| author | Jon French | 2018-05-09 14:08:42 +0100 |
|---|---|---|
| committer | Jon French | 2018-05-09 14:08:42 +0100 |
| commit | 86e6b9e26b76e4af4e5ba056b2e5e7efc98b8efd (patch) | |
| tree | be4db8108ef17b8e416e4b5065bb70539fdbbbfd /riscv/prelude.sail | |
| parent | b6b21038c2f287a54a8bb29ec555cc42bb809100 (diff) | |
start of riscv assembly mappings
Diffstat (limited to 'riscv/prelude.sail')
| -rw-r--r-- | riscv/prelude.sail | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/riscv/prelude.sail b/riscv/prelude.sail index d667573e..6a627d22 100644 --- a/riscv/prelude.sail +++ b/riscv/prelude.sail @@ -3,6 +3,10 @@ default Order dec type bits ('n : Int) = vector('n, dec, bit) union option ('a : Type) = {None : unit, Some : 'a} +val spaces : nat <-> string +val opt_spaces : nat <-> string +val hex_bits : forall 'n. (atom('n), bits('n)) <-> string + val eq_atom = {ocaml: "eq_int", lem: "eq", c: "eq_int"} : forall 'n 'm. (atom('n), atom('m)) -> bool val lteq_atom = "lteq" : forall 'n 'm. (atom('n), atom('m)) -> bool val gteq_atom = "gteq" : forall 'n 'm. (atom('n), atom('m)) -> bool |