4 files changed, 19 insertions, 8 deletions
diff --git a/lib/arith.sail b/lib/arith.sail
index b233048e..8825ac2f 100644
--- a/lib/arith.sail
+++ b/lib/arith.sail
@@ -102,6 +102,7 @@ val abs_int = {
   smt : "abs",
   ocaml: "abs_int",
   lem: "abs_int",
+  c: "abs_int",
   coq: "Z.abs"
 } : (int, int) -> int
 
diff --git a/lib/flow.sail b/lib/flow.sail
index cb77f5b1..e6fe7fc0 100644
--- a/lib/flow.sail
+++ b/lib/flow.sail
@@ -50,4 +50,15 @@ overload operator < = {lt_int}
 overload operator >= = {gteq_int}
 overload operator > = {gt_int}
 
+/*
+
+when we have sizeof('n) where x : int('n), we can remove that sizeof
+by rewriting it to __size(x).
+
+*/
+
+function __id forall 'n. (x: int('n)) -> int('n) = x
+
+overload __size = {__id}
+
 $endif
diff --git a/lib/smt.sail b/lib/smt.sail
index 6a5a1327..d886c127 100644
--- a/lib/smt.sail
+++ b/lib/smt.sail
@@ -4,36 +4,33 @@ $define _SMT
 // see http://smtlib.cs.uiowa.edu/theories-Ints.shtml
 
 val div = {
-  smt: "div",
   ocaml: "quotient",
   lem: "integerDiv",
   c: "tdiv_int",
   coq: "ediv_with_eq"
-} : forall 'n 'm. (atom('n), atom('m)) -> atom(div('n, 'm)) // {'o, 'o == div('n, 'm). atom('o)}
+} : forall 'n 'm. (int('n), int('m)) -> int(div('n, 'm))
 
 overload operator / = {div}
 
 val mod = {
-  smt: "mod",
   ocaml: "modulus",
   lem: "integerMod",
   c: "tmod_int",
   coq: "emod_with_eq"
-} : forall 'n 'm. (atom('n), atom('m)) -> atom(mod('n, 'm))
+} : forall 'n 'm. (int('n), int('m)) -> int(mod('n, 'm))
 
 overload operator % = {mod}
 
-val abs_atom = {
-  smt : "abs",
+val abs_int = {
   ocaml: "abs_int",
   lem: "abs_int",
   c: "abs_int",
   coq: "abs_with_eq"
-} : forall 'n. atom('n) -> atom(abs('n))
+} : forall 'n. int('n) -> int(abs('n))
 
 $ifdef TEST
 
-let __smt_x : atom(div(4, 2)) = div(8, 4)
+let __smt_x : int(div(4, 2)) = div(8, 4)
 
 $endif
 
diff --git a/lib/vector_dec.sail b/lib/vector_dec.sail
index 4e4bad5a..166db243 100644
--- a/lib/vector_dec.sail
+++ b/lib/vector_dec.sail
@@ -166,4 +166,6 @@ val signed = {
   _: "sint"
 } : forall 'n, 'n > 0. bits('n) -> range(- (2 ^ ('n - 1)), 2 ^ ('n - 1) - 1)
 
+overload __size = {length}
+
 $endif