diff options
Diffstat (limited to 'aarch64_small')
| -rw-r--r-- | aarch64_small/armV8.h.sail | 2 | ||||
| -rw-r--r-- | aarch64_small/prelude.sail | 7 |
2 files changed, 2 insertions, 7 deletions
diff --git a/aarch64_small/armV8.h.sail b/aarch64_small/armV8.h.sail index d0f0b830..8b38f2eb 100644 --- a/aarch64_small/armV8.h.sail +++ b/aarch64_small/armV8.h.sail @@ -32,8 +32,6 @@ /* SUCH DAMAGE. */ /*========================================================================*/ -default Order dec - type boolean = bit type integer = int type uinteger = nat /* ARM ARM does not have nat/uint type */ diff --git a/aarch64_small/prelude.sail b/aarch64_small/prelude.sail index d94112ad..c904aec6 100644 --- a/aarch64_small/prelude.sail +++ b/aarch64_small/prelude.sail @@ -1,9 +1,8 @@ +default Order dec + let b1 = bitone let b0 = bitzero - -/* default Order dec */ - val "reg_deref" : forall ('a : Type). register('a) -> 'a effect {rreg} /* sneaky deref with no effect necessary for bitfield writes */ val _reg_deref = "reg_deref" : forall ('a : Type). register('a) -> 'a @@ -13,8 +12,6 @@ val _reg_deref = "reg_deref" : forall ('a : Type). register('a) -> 'a /* val eq_bit2 = "eq_bit" : (bit, bit) -> bool */ /* overload operator == = {eq_bit2} */ - - $include <smt.sail> $include <flow.sail> $include <arith.sail> |