diff --git a/library/init/data/to_string.lean b/library/init/data/to_string.lean
index 568a57e1b1..07db575213 100644
--- a/library/init/data/to_string.lean
+++ b/library/init/data/to_string.lean
@@ -61,6 +61,9 @@ instance : has_to_string uint32 :=
 instance : has_to_string uint64 :=
 ⟨λ n, to_string n.to_nat⟩
 
+instance : has_to_string usize :=
+⟨λ n, to_string n.to_nat⟩
+
 instance {α : Type u} [has_to_string α] : has_to_string (option α) :=
 ⟨λ o, match o with | none := "none" | (some a) := "(some " ++ to_string a ++ ")"⟩
 
diff --git a/library/init/lean/format.lean b/library/init/lean/format.lean
index 87499f1444..484a51bb1c 100644
--- a/library/init/lean/format.lean
+++ b/library/init/lean/format.lean
@@ -136,6 +136,7 @@ instance nat_has_to_format : has_to_format nat    := ⟨λ n, to_string n⟩
 instance uint16_has_to_format : has_to_format uint16 := ⟨λ n, to_string n⟩
 instance uint32_has_to_format : has_to_format uint32 := ⟨λ n, to_string n⟩
 instance uint64_has_to_format : has_to_format uint64 := ⟨λ n, to_string n⟩
+instance usize_has_to_format : has_to_format usize := ⟨λ n, to_string n⟩
 
 instance format_has_to_string : has_to_string format := ⟨pretty⟩
 
diff --git a/library/init/lean/ir/extract_cpp.lean b/library/init/lean/ir/extract_cpp.lean
index 55af467604..56f6f991dd 100644
--- a/library/init/lean/ir/extract_cpp.lean
+++ b/library/init/lean/ir/extract_cpp.lean
@@ -126,10 +126,6 @@ def emit_call_lhs : list var → extract_m unit
 def emit_type_size (ty : type) : extract_m unit :=
 emit "sizeof" >> paren(emit_type ty)
 
-def emit_sizet : list (nat × type) → extract_m unit
-| []             := emit 0
-| ((n, ty)::ss)  := emit n >> emit "*" >> emit_type_size ty >> emit " + " >> emit_sizet ss
-
 /-- Emit `op(x)` -/
 def emit_op_x (op : string) (x : var) : extract_m unit :=
 emit op >> paren (emit_var x)
@@ -234,11 +230,11 @@ ins.decorate_error $
  | (instr.unop x t op y)     := emit_unop x t op y
  | (instr.binop x t op y z)  := emit_binop x t op y z
  | (instr.call xs f ys)      := emit_call_lhs xs >> emit_fnid f >> paren(emit_var_list ys)
- | (instr.cnstr o t n sz)    := emit_var o >> emit " := lean::alloc_cnstr" >> paren(emit t <+> emit n <+> emit_sizet sz)
+ | (instr.cnstr o t n sz)    := emit_var o >> emit " := lean::alloc_cnstr" >> paren(emit t <+> emit n <+> emit sz)
  | (instr.set o i x)         := emit "lean::set_cnstr_obj" >> paren (emit_var o <+> emit i <+> emit_var x)
  | (instr.get x o i)         := emit_var x >> emit " := lean::cnstr_obj" >> paren(emit_var o <+> emit i)
- | (instr.sset o d x)        := emit "lean::set_cnstr_scalar" >> paren(emit_var o <+> emit_sizet d <+> emit_var x)
- | (instr.sget x t o d)      := emit_var x >> emit " := lean::cnstr_scalar" >> emit_template_param t >> paren(emit_var o <+> emit_sizet d)
+ | (instr.sset o d x)        := emit "lean::set_cnstr_scalar" >> paren(emit_var o <+> emit d <+> emit_var x)
+ | (instr.sget x t o d)      := emit_var x >> emit " := lean::cnstr_scalar" >> emit_template_param t >> paren(emit_var o <+> emit d)
  | (instr.closure x f ys)    := return () -- TODO
  | (instr.apply x ys)        := return () -- TODO
  | (instr.array a sz c)      := emit_var a >> emit " := lean::alloc_array" >> paren(emit_var sz <+> emit_var c)
diff --git a/library/init/lean/ir/format.lean b/library/init/lean/ir/format.lean
index c49f45bb0c..c7745eaf39 100644
--- a/library/init/lean/ir/format.lean
+++ b/library/init/lean/ir/format.lean
@@ -92,12 +92,6 @@ def sizet_entry.to_format : nat × type → format
 | (1, ty) := to_fmt ty
 | (n, ty) := to_fmt n ++ ":" ++ to_fmt ty
 
-def sizet.to_format (s : sizet) : format :=
-sbracket $ join_sep (s.map sizet_entry.to_format) ("," ++ line)
-
-instance sizet.has_to_format : has_to_format sizet := ⟨sizet.to_format⟩
-instance sizet.has_to_string : has_to_string sizet := ⟨pretty ∘ to_fmt⟩
-
 def instr.to_format : instr → format
 | (instr.lit x ty lit)       := to_fmt x ++ " : " ++ to_fmt ty ++ " := " ++ to_fmt lit
 | (instr.unop x ty op y)     := to_fmt x ++ " : " ++ to_fmt ty ++ " := " ++ to_fmt op ++ " " ++ to_fmt y
diff --git a/library/init/lean/ir/ir.lean b/library/init/lean/ir/ir.lean
index 0cbff904fd..e995a81790 100644
--- a/library/init/lean/ir/ir.lean
+++ b/library/init/lean/ir/ir.lean
@@ -81,13 +81,6 @@ def tag     := uint16
 def var     := name
 def fnid    := name
 def blockid := name
-/--
-`sizet` is used to represent object size and offset.
-An element `[(n_1, t_1), ..., (n_k, t_k)]` represents
-the size/offset `n_1 * sizeof(t_1) + ... + n_k * sizeof(t_k)`.
-We use this type to be able to generate platform independent
-code because the size of some types are platform dependent (e.g., `object` and `usize`) -/
-def sizet   := list (nat × type)
 
 instance var_has_lt : has_lt var := (name.has_lt_quick : has_lt name)
 instance blockid_has_lt : has_lt blockid := (name.has_lt_quick : has_lt name)
@@ -116,11 +109,11 @@ inductive instr
 | binop   (x : var) (ty : type) (op : binop) (y z : var)        -- x : ty := op y z
 | call    (xs : list var) (f : fnid) (ys : list var)            -- Function call:  xs := f ys
 /- Constructor objects -/
-| cnstr   (o : var) (tag : tag) (nobjs : uint16) (ssz : sizet)  -- Create constructor object
+| cnstr   (o : var) (tag : tag) (nobjs : uint16) (ssz : usize)  -- Create constructor object
 | set     (o : var) (i : uint16) (x : var)                      -- Set object field:          set o i x
 | get     (x : var) (o : var) (i : uint16)                      -- Get object field:          x := get o i
-| sset    (o : var) (d : sizet) (v : var)                       -- Set scalar field:          sset o d v
-| sget    (x : var) (ty : type) (o : var) (d : sizet)           -- Get scalar field:          x : ty := sget o d
+| sset    (o : var) (d : usize) (v : var)                       -- Set scalar field:          sset o d v
+| sget    (x : var) (ty : type) (o : var) (d : usize)           -- Get scalar field:          x : ty := sget o d
 /- Closures -/
 | closure (x : var) (f : fnid) (ys : list var)                  -- Create closure:            x := closure f ys
 | apply   (x : var) (ys : list var)                             -- Apply closure:             x := apply ys
diff --git a/library/init/lean/ir/parser.lean b/library/init/lean/ir/parser.lean
index 828142b56e..1d836009a9 100644
--- a/library/init/lean/ir/parser.lean
+++ b/library/init/lean/ir/parser.lean
@@ -89,6 +89,13 @@ try (do p ← pos,
         return $ uint16.of_nat n)
 <?> "uint16"
 
+def parse_usize : parser usize :=
+try (do p ← pos,
+        n ← lexeme num,
+        when (n ≥ usize_sz) $ unexpected_at "big numeral, it does not fit in an usize" p,
+        return $ usize.of_nat n)
+<?> "usize"
+
 def identifier : parser name :=
 try (do p ← pos,
         n ← lean.parser.identifier,
@@ -113,19 +120,11 @@ do xs  ← many1 parse_var,
    ys  ← many parse_var,
    return $ instr.call ([x] ++ xs) fid ys
 
-def parse_sizet_entry : parser (nat × type) :=
-(prod.mk 1 <$> parse_type)
-<|>
-(prod.mk <$> (lexeme num <?> "numeral") <*> (symbol ":" >> parse_type))
-
-def parse_sizet : parser sizet :=
-symbol "[" >> sep_by parse_sizet_entry (symbol ",") <* symbol "]"
-
 def parse_typed_assignment (x : var) : parser instr :=
 do  symbol ":",
     ty ← parse_type,
     symbol ":=",
-    (keyword "sget" >> instr.sget x ty <$> parse_var <*> parse_sizet)
+    (keyword "sget" >> instr.sget x ty <$> parse_var <*> parse_usize)
 <|> (instr.unop x ty <$> parse_unop <*> parse_var)
 <|> (instr.binop x ty <$> parse_binop <*> parse_var <*> parse_var)
 <|> (instr.lit x ty <$> parse_literal)
@@ -136,7 +135,7 @@ do  symbol ":=",
 <|> (keyword "apply"   >> instr.apply x <$> many1 parse_var)
 <|> (keyword "get"     >> instr.get x <$> parse_var <*> parse_uint16)
 <|> (keyword "call"    >> instr.call [x] <$> parse_fnid <*> many parse_var)
-<|> (keyword "cnstr"   >> instr.cnstr x <$> parse_uint16 <*> parse_uint16 <*> parse_sizet)
+<|> (keyword "cnstr"   >> instr.cnstr x <$> parse_uint16 <*> parse_uint16 <*> parse_usize)
 <|> (keyword "array"   >> instr.array x <$> parse_var <*> parse_var)
 <|> (keyword "sarray"  >> instr.sarray x <$> parse_type <*> parse_var <*> parse_var)
 
@@ -150,7 +149,7 @@ def parse_instr : parser instr :=
     (keyword "array_write" >> instr.array_write <$> parse_var <*> parse_var <*> parse_var)
 <|> (keyword "array_push" >> instr.array_push <$> parse_var <*> parse_var)
 <|> (keyword "set" >> instr.set <$> parse_var <*> parse_uint16 <*> parse_var)
-<|> (keyword "sset" >> instr.sset <$> parse_var <*> parse_sizet <*> parse_var)
+<|> (keyword "sset" >> instr.sset <$> parse_var <*> parse_usize <*> parse_var)
 <|> (instr.unary <$> parse_unins <*> parse_var)
 <|> parse_assignment
 
diff --git a/tests/lean/parser1.lean b/tests/lean/parser1.lean
index c3bc9a5d37..67b2e202dc 100644
--- a/tests/lean/parser1.lean
+++ b/tests/lean/parser1.lean
@@ -104,11 +104,11 @@ do cmd ← lean.ir.parse_instr,
 #eval test parse_instr_pp "x : bool := and z   y" "x : bool := and z y"
 #eval test parse_instr_pp "x y := call f z w" "x y := call f z w"
 #eval test parse_instr_pp "x := call f z   w" "x := call f z w"
-#eval test parse_instr_pp "o := cnstr 0   3   []" "o := cnstr 0 3 []"
+#eval test parse_instr_pp "o := cnstr 0   3   0" "o := cnstr 0 3 0"
 #eval test parse_instr_pp "set o 0 x" "set o 0 x"
 #eval test parse_instr_pp "x := get o 0" "x := get o 0"
-#eval test parse_instr_pp "sset o [object] x" "sset o [object] x"
-#eval test parse_instr_pp "x : bool := sget o [object, 2:usize]" "x : bool := sget o [object, 2:usize]"
+#eval test parse_instr_pp "sset o 8 x" "sset o 8 x"
+#eval test parse_instr_pp "x : bool := sget o 24" "x : bool := sget o 24"
 #eval test parse_instr_pp "x := closure f a" "x := closure f a"
 #eval test parse_instr_pp "x := closure f a b" "x := closure f a b"
 #eval test parse_instr_pp "x := apply f a" "x := apply f a"
diff --git a/tests/lean/run/parser_ir1.lean b/tests/lean/run/parser_ir1.lean
index fd5ac3d9c6..4de7a5f638 100644
--- a/tests/lean/run/parser_ir1.lean
+++ b/tests/lean/run/parser_ir1.lean
@@ -53,13 +53,13 @@ do (except.ok d) ← return $ parse (whitespace >> parse_def) s,
 def IR3 := "
 def mk_struct (d1 : object) (d2 : uint32) (d3 : usize) (d4 : uint32) (d5 : bool) (d6 : bool) : object :=
 main:
-  o := cnstr 0 1 [object, 2:uint32, usize, bool];
+  o := cnstr 0 1 18;
   set o 0 d1;
-  sset o [object] d3;
-  sset o [object, usize] d2;
-  sset o [object, usize, uint32] d4;
-  sset o [object, usize, 2:uint32] d5;
-  sset o [object, usize, 2:uint32, bool] d6;
+  sset o 8 d3;
+  sset o 16 d2;
+  sset o 20 d4;
+  sset o 24 d5;
+  sset o 25 d6;
   ret o;
 "
 #eval show_result (whitespace >> parse_def) IR3
@@ -76,8 +76,8 @@ do (except.ok d) ← return $ parse (whitespace >> parse_def) s,
 def IR4 := "
 def swap (d1 : object) (d2 : object) : object object :=
 main:
-  r1 := cnstr 0 2 [];
-  r2 := cnstr 0 2 [];
+  r1 := cnstr 0 2 0;
+  r2 := cnstr 0 2 0;
   set r1 0 d1;
   set r1 1 d2;
   inc d1;