diff options
| author | Alasdair Armstrong | 2018-03-19 17:39:42 +0000 |
|---|---|---|
| committer | Alasdair Armstrong | 2018-03-19 17:39:42 +0000 |
| commit | b42d5ab44307da291aac1882f8a2bb7bcbdfa900 (patch) | |
| tree | eddf168eca14f33ddd34027b0553302612a679da /riscv/prelude.sail | |
| parent | e3e597feb532c71e0db32eb9abbebb9f51314d6d (diff) | |
Fixes to C backend for RISCV-compilation
Can now compile RISCV. Requires some library tweaks before it'll pass any tests,
Also adds hyperlinks to wip latex output
Diffstat (limited to 'riscv/prelude.sail')
| -rw-r--r-- | riscv/prelude.sail | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/riscv/prelude.sail b/riscv/prelude.sail index f6532215..44791217 100644 --- a/riscv/prelude.sail +++ b/riscv/prelude.sail @@ -3,7 +3,7 @@ default Order dec type bits ('n : Int) = vector('n, dec, bit) 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 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 val lt_atom = "lt" : forall 'n 'm. (atom('n), atom('m)) -> bool |