diff --git a/src/Init/Data/Float.lean b/src/Init/Data/Float.lean
index 9b0d86e53b..8d64928439 100644
--- a/src/Init/Data/Float.lean
+++ b/src/Init/Data/Float.lean
@@ -32,11 +32,11 @@ structure Float where
 instance : Inhabited Float := ⟨{ val := floatSpec.val }⟩
 
 @[extern "lean_float_of_nat"] constant Float.ofNat : (@& Nat) → Float
-@[extern c inline "#1 + #2"]  constant Float.add : Float → Float → Float
-@[extern c inline "#1 - #2"]  constant Float.sub : Float → Float → Float
-@[extern c inline "#1 * #2"]  constant Float.mul : Float → Float → Float
-@[extern c inline "#1 / #2"]  constant Float.div : Float → Float → Float
-@[extern c inline "(- #1)"]   constant Float.neg : Float → Float
+@[extern "lean_float_add"]  constant Float.add : Float → Float → Float
+@[extern "lean_float_sub"]  constant Float.sub : Float → Float → Float
+@[extern "lean_float_mul"]  constant Float.mul : Float → Float → Float
+@[extern "lean_float_div"]  constant Float.div : Float → Float → Float
+@[extern "lean_float_negate"]   constant Float.neg : Float → Float
 
 def Float.ofInt : Int → Float
   | Int.ofNat n => Float.ofNat n
@@ -59,15 +59,15 @@ instance : Neg Float       := ⟨Float.neg⟩
 instance : LT Float        := ⟨Float.lt⟩
 instance : LE Float        := ⟨Float.le⟩
 
-@[extern c inline "#1 == #2"] constant Float.beq (a b : Float) : Bool
+@[extern "lean_float_beq"] constant Float.beq (a b : Float) : Bool
 
 instance : BEq Float := ⟨Float.beq⟩
 
-@[extern c inline "#1 < #2"]   constant Float.decLt (a b : Float) : Decidable (a < b) :=
+@[extern "lean_float_decLt"]   constant Float.decLt (a b : Float) : Decidable (a < b) :=
   match a, b with
   | ⟨a⟩, ⟨b⟩ => floatSpec.decLt a b
 
-@[extern c inline "#1 <= #2"] constant Float.decLe (a b : Float) : Decidable (a ≤ b) :=
+@[extern "lean_float_decLe"] constant Float.decLe (a b : Float) : Decidable (a ≤ b) :=
   match a, b with
   | ⟨a⟩, ⟨b⟩ => floatSpec.decLe a b
 
@@ -76,11 +76,11 @@ instance floatDecLe (a b : Float) : Decidable (a ≤ b) := Float.decLe a b
 
 @[extern "lean_float_to_string"] constant Float.toString : Float → String
 
-@[extern c inline "(uint8_t)#1"] constant Float.toUInt8 : Float → UInt8
-@[extern c inline "(uint16_t)#1"] constant Float.toUInt16 : Float → UInt16
-@[extern c inline "(uint32_t)#1"] constant Float.toUInt32 : Float → UInt32
-@[extern c inline "(uint64_t)#1"] constant Float.toUInt64 : Float → UInt64
-@[extern c inline "(size_t)#1"] constant Float.toUSize : Float → USize
+@[extern "lean_float_to_uint8"] constant Float.toUInt8 : Float → UInt8
+@[extern "lean_float_to_uint16"] constant Float.toUInt16 : Float → UInt16
+@[extern "lean_float_to_uint32"] constant Float.toUInt32 : Float → UInt32
+@[extern "lean_float_to_uint64"] constant Float.toUInt64 : Float → UInt64
+@[extern "lean_float_to_usize"] constant Float.toUSize : Float → USize
 
 instance : ToString Float where
   toString := Float.toString
diff --git a/src/Init/Data/UInt.lean b/src/Init/Data/UInt.lean
index e99f6e08d4..9fef30a94c 100644
--- a/src/Init/Data/UInt.lean
+++ b/src/Init/Data/UInt.lean
@@ -14,27 +14,27 @@ def UInt8.ofNat (n : @& Nat) : UInt8 := ⟨Fin.ofNat n⟩
 abbrev Nat.toUInt8 := UInt8.ofNat
 @[extern "lean_uint8_to_nat"]
 def UInt8.toNat (n : UInt8) : Nat := n.val.val
-@[extern c inline "#1 + #2"]
+@[extern "lean_uint8_add"]
 def UInt8.add (a b : UInt8) : UInt8 := ⟨a.val + b.val⟩
-@[extern c inline "#1 - #2"]
+@[extern "lean_uint8_sub"]
 def UInt8.sub (a b : UInt8) : UInt8 := ⟨a.val - b.val⟩
-@[extern c inline "#1 * #2"]
+@[extern "lean_uint8_mul"]
 def UInt8.mul (a b : UInt8) : UInt8 := ⟨a.val * b.val⟩
-@[extern c inline "#2 == 0 ? 0 : #1 / #2"]
+@[extern "lean_uint8_div"]
 def UInt8.div (a b : UInt8) : UInt8 := ⟨a.val / b.val⟩
-@[extern c inline "#2 == 0 ? #1 : #1 % #2"]
+@[extern "lean_uint8_mod"]
 def UInt8.mod (a b : UInt8) : UInt8 := ⟨a.val % b.val⟩
 @[extern "lean_uint8_modn"]
 def UInt8.modn (a : UInt8) (n : @& Nat) : UInt8 := ⟨a.val % n⟩
-@[extern c inline "#1 & #2"]
+@[extern "lean_uint8_land"]
 def UInt8.land (a b : UInt8) : UInt8 := ⟨Fin.land a.val b.val⟩
-@[extern c inline "#1 | #2"]
+@[extern "lean_uint8_lor"]
 def UInt8.lor (a b : UInt8) : UInt8 := ⟨Fin.lor a.val b.val⟩
-@[extern c inline "#1 ^ #2"]
+@[extern "lean_uint8_xor"]
 def UInt8.xor (a b : UInt8) : UInt8 := ⟨Fin.xor a.val b.val⟩
-@[extern c inline "#1 << #2 % 8"]
+@[extern "lean_uint8_shift_left"]
 def UInt8.shiftLeft (a b : UInt8) : UInt8 := ⟨a.val <<< (modn b 8).val⟩
-@[extern c inline "#1 >> #2 % 8"]
+@[extern "lean_uint8_shift_right"]
 def UInt8.shiftRight (a b : UInt8) : UInt8 := ⟨a.val >>> (modn b 8).val⟩
 def UInt8.lt (a b : UInt8) : Prop := a.val < b.val
 def UInt8.le (a b : UInt8) : Prop := a.val ≤ b.val
@@ -49,7 +49,7 @@ instance : Div UInt8       := ⟨UInt8.div⟩
 instance : LT UInt8        := ⟨UInt8.lt⟩
 instance : LE UInt8        := ⟨UInt8.le⟩
 
-@[extern c inline "~ #1"]
+@[extern "lean_uint8_complement"]
 def UInt8.complement (a:UInt8) : UInt8 := 0-(a+1)
 
 instance : Complement UInt8 := ⟨UInt8.complement⟩
@@ -60,13 +60,13 @@ instance : ShiftLeft UInt8  := ⟨UInt8.shiftLeft⟩
 instance : ShiftRight UInt8 := ⟨UInt8.shiftRight⟩
 
 set_option bootstrap.genMatcherCode false in
-@[extern c inline "#1 < #2"]
+@[extern "lean_uint8_dec_lt"]
 def UInt8.decLt (a b : UInt8) : Decidable (a < b) :=
   match a, b with
   | ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (n < m))
 
 set_option bootstrap.genMatcherCode false in
-@[extern c inline "#1 <= #2"]
+@[extern "lean_uint8_dec_le"]
 def UInt8.decLe (a b : UInt8) : Decidable (a ≤ b) :=
   match a, b with
   | ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (n <= m))
@@ -79,31 +79,31 @@ def UInt16.ofNat (n : @& Nat) : UInt16 := ⟨Fin.ofNat n⟩
 abbrev Nat.toUInt16 := UInt16.ofNat
 @[extern "lean_uint16_to_nat"]
 def UInt16.toNat (n : UInt16) : Nat := n.val.val
-@[extern c inline "#1 + #2"]
+@[extern "lean_uint16_add"]
 def UInt16.add (a b : UInt16) : UInt16 := ⟨a.val + b.val⟩
-@[extern c inline "#1 - #2"]
+@[extern "lean_uint16_sub"]
 def UInt16.sub (a b : UInt16) : UInt16 := ⟨a.val - b.val⟩
-@[extern c inline "#1 * #2"]
+@[extern "lean_uint16_mul"]
 def UInt16.mul (a b : UInt16) : UInt16 := ⟨a.val * b.val⟩
-@[extern c inline "#2 == 0 ? 0 : #1 / #2"]
+@[extern "lean_uint16_div"]
 def UInt16.div (a b : UInt16) : UInt16 := ⟨a.val / b.val⟩
-@[extern c inline "#2 == 0 ? #1 : #1 % #2"]
+@[extern "lean_uint16_mod"]
 def UInt16.mod (a b : UInt16) : UInt16 := ⟨a.val % b.val⟩
 @[extern "lean_uint16_modn"]
 def UInt16.modn (a : UInt16) (n : @& Nat) : UInt16 := ⟨a.val % n⟩
-@[extern c inline "#1 & #2"]
+@[extern "lean_uint16_land"]
 def UInt16.land (a b : UInt16) : UInt16 := ⟨Fin.land a.val b.val⟩
-@[extern c inline "#1 | #2"]
+@[extern "lean_uint16_lor"]
 def UInt16.lor (a b : UInt16) : UInt16 := ⟨Fin.lor a.val b.val⟩
-@[extern c inline "#1 ^ #2"]
+@[extern "lean_uint16_xor"]
 def UInt16.xor (a b : UInt16) : UInt16 := ⟨Fin.xor a.val b.val⟩
-@[extern c inline "#1 << #2 % 16"]
+@[extern "lean_uint16_shift_left"]
 def UInt16.shiftLeft (a b : UInt16) : UInt16 := ⟨a.val <<< (modn b 16).val⟩
-@[extern c inline "((uint8_t)#1)"]
+@[extern "lean_uint16_to_uint8"]
 def UInt16.toUInt8 (a : UInt16) : UInt8 := a.toNat.toUInt8
-@[extern c inline "((uint16_t)#1)"]
+@[extern "lean_uint8_to_uint16"]
 def UInt8.toUInt16 (a : UInt8) : UInt16 := a.toNat.toUInt16
-@[extern c inline "#1 >> #2 % 16"]
+@[extern "lean_uint16_shift_right"]
 def UInt16.shiftRight (a b : UInt16) : UInt16 := ⟨a.val >>> (modn b 16).val⟩
 def UInt16.lt (a b : UInt16) : Prop := a.val < b.val
 def UInt16.le (a b : UInt16) : Prop := a.val ≤ b.val
@@ -119,7 +119,7 @@ instance : Div UInt16       := ⟨UInt16.div⟩
 instance : LT UInt16        := ⟨UInt16.lt⟩
 instance : LE UInt16        := ⟨UInt16.le⟩
 
-@[extern c inline "~ #1"]
+@[extern "lean_uint16_complement"]
 def UInt16.complement (a:UInt16) : UInt16 := 0-(a+1)
 
 instance : Complement UInt16 := ⟨UInt16.complement⟩
@@ -130,13 +130,13 @@ instance : ShiftLeft UInt16  := ⟨UInt16.shiftLeft⟩
 instance : ShiftRight UInt16 := ⟨UInt16.shiftRight⟩
 
 set_option bootstrap.genMatcherCode false in
-@[extern c inline "#1 < #2"]
+@[extern "lean_uint16_dec_lt"]
 def UInt16.decLt (a b : UInt16) : Decidable (a < b) :=
   match a, b with
   | ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (n < m))
 
 set_option bootstrap.genMatcherCode false in
-@[extern c inline "#1 <= #2"]
+@[extern "lean_uint16_dec_le"]
 def UInt16.decLe (a b : UInt16) : Decidable (a ≤ b) :=
   match a, b with
   | ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (n <= m))
@@ -149,35 +149,35 @@ def UInt32.ofNat (n : @& Nat) : UInt32 := ⟨Fin.ofNat n⟩
 @[extern "lean_uint32_of_nat"]
 def UInt32.ofNat' (n : Nat) (h : n < UInt32.size) : UInt32 := ⟨⟨n, h⟩⟩
 abbrev Nat.toUInt32 := UInt32.ofNat
-@[extern c inline "#1 + #2"]
+@[extern "lean_uint32_add"]
 def UInt32.add (a b : UInt32) : UInt32 := ⟨a.val + b.val⟩
-@[extern c inline "#1 - #2"]
+@[extern "lean_uint32_sub"]
 def UInt32.sub (a b : UInt32) : UInt32 := ⟨a.val - b.val⟩
-@[extern c inline "#1 * #2"]
+@[extern "lean_uint32_mul"]
 def UInt32.mul (a b : UInt32) : UInt32 := ⟨a.val * b.val⟩
-@[extern c inline "#2 == 0 ? 0 : #1 / #2"]
+@[extern "lean_uint32_div"]
 def UInt32.div (a b : UInt32) : UInt32 := ⟨a.val / b.val⟩
-@[extern c inline "#2 == 0 ? #1 : #1 % #2"]
+@[extern "lean_uint32_mod"]
 def UInt32.mod (a b : UInt32) : UInt32 := ⟨a.val % b.val⟩
 @[extern "lean_uint32_modn"]
 def UInt32.modn (a : UInt32) (n : @& Nat) : UInt32 := ⟨a.val % n⟩
-@[extern c inline "#1 & #2"]
+@[extern "lean_uint32_land"]
 def UInt32.land (a b : UInt32) : UInt32 := ⟨Fin.land a.val b.val⟩
-@[extern c inline "#1 | #2"]
+@[extern "lean_uint32_lor"]
 def UInt32.lor (a b : UInt32) : UInt32 := ⟨Fin.lor a.val b.val⟩
-@[extern c inline "#1 ^ #2"]
+@[extern "lean_uint32_xor"]
 def UInt32.xor (a b : UInt32) : UInt32 := ⟨Fin.xor a.val b.val⟩
-@[extern c inline "#1 << #2 % 32"]
+@[extern "lean_uint32_shift_left"]
 def UInt32.shiftLeft (a b : UInt32) : UInt32 := ⟨a.val <<< (modn b 32).val⟩
-@[extern c inline "#1 >> #2 % 32"]
+@[extern "lean_uint32_shift_right"]
 def UInt32.shiftRight (a b : UInt32) : UInt32 := ⟨a.val >>> (modn b 32).val⟩
-@[extern c inline "((uint8_t)#1)"]
+@[extern "lean_uint32_to_uint8"]
 def UInt32.toUInt8 (a : UInt32) : UInt8 := a.toNat.toUInt8
-@[extern c inline "((uint16_t)#1)"]
+@[extern "lean_uint32_to_uint16"]
 def UInt32.toUInt16 (a : UInt32) : UInt16 := a.toNat.toUInt16
-@[extern c inline "((uint32_t)#1)"]
+@[extern "lean_uint8_to_uint32"]
 def UInt8.toUInt32 (a : UInt8) : UInt32 := a.toNat.toUInt32
-@[extern c inline "((uint32_t)#1)"]
+@[extern "lean_uint16_to_uint32"]
 def UInt16.toUInt32 (a : UInt16) : UInt32 := a.toNat.toUInt32
 
 instance : OfNat UInt32 n   := ⟨UInt32.ofNat n⟩
@@ -188,7 +188,7 @@ instance : Mod UInt32       := ⟨UInt32.mod⟩
 instance : HMod UInt32 Nat UInt32 := ⟨UInt32.modn⟩
 instance : Div UInt32       := ⟨UInt32.div⟩
 
-@[extern c inline "~ #1"]
+@[extern "lean_uint32_complement"]
 def UInt32.complement (a:UInt32) : UInt32 := 0-(a+1)
 
 instance : Complement UInt32 := ⟨UInt32.complement⟩
@@ -203,41 +203,41 @@ def UInt64.ofNat (n : @& Nat) : UInt64 := ⟨Fin.ofNat n⟩
 abbrev Nat.toUInt64 := UInt64.ofNat
 @[extern "lean_uint64_to_nat"]
 def UInt64.toNat (n : UInt64) : Nat := n.val.val
-@[extern c inline "#1 + #2"]
+@[extern "lean_uint64_add"]
 def UInt64.add (a b : UInt64) : UInt64 := ⟨a.val + b.val⟩
-@[extern c inline "#1 - #2"]
+@[extern "lean_uint64_sub"]
 def UInt64.sub (a b : UInt64) : UInt64 := ⟨a.val - b.val⟩
-@[extern c inline "#1 * #2"]
+@[extern "lean_uint64_mul"]
 def UInt64.mul (a b : UInt64) : UInt64 := ⟨a.val * b.val⟩
-@[extern c inline "#2 == 0 ? 0 : #1 / #2"]
+@[extern "lean_uint64_div"]
 def UInt64.div (a b : UInt64) : UInt64 := ⟨a.val / b.val⟩
-@[extern c inline "#2 == 0 ? #1 : #1 % #2"]
+@[extern "lean_uint64_mod"]
 def UInt64.mod (a b : UInt64) : UInt64 := ⟨a.val % b.val⟩
 @[extern "lean_uint64_modn"]
 def UInt64.modn (a : UInt64) (n : @& Nat) : UInt64 := ⟨a.val % n⟩
-@[extern c inline "#1 & #2"]
+@[extern "lean_uint64_land"]
 def UInt64.land (a b : UInt64) : UInt64 := ⟨Fin.land a.val b.val⟩
-@[extern c inline "#1 | #2"]
+@[extern "lean_uint64_lor"]
 def UInt64.lor (a b : UInt64) : UInt64 := ⟨Fin.lor a.val b.val⟩
-@[extern c inline "#1 ^ #2"]
+@[extern "lean_uint64_xor"]
 def UInt64.xor (a b : UInt64) : UInt64 := ⟨Fin.xor a.val b.val⟩
-@[extern c inline "#1 << #2 % 64"]
+@[extern "lean_uint64_shift_left"]
 def UInt64.shiftLeft (a b : UInt64) : UInt64 := ⟨a.val <<< (modn b 64).val⟩
-@[extern c inline "#1 >> #2 % 64"]
+@[extern "lean_uint64_shift_right"]
 def UInt64.shiftRight (a b : UInt64) : UInt64 := ⟨a.val >>> (modn b 64).val⟩
 def UInt64.lt (a b : UInt64) : Prop := a.val < b.val
 def UInt64.le (a b : UInt64) : Prop := a.val ≤ b.val
-@[extern c inline "((uint8_t)#1)"]
+@[extern "lean_uint64_to_uint8"]
 def UInt64.toUInt8 (a : UInt64) : UInt8 := a.toNat.toUInt8
-@[extern c inline "((uint16_t)#1)"]
+@[extern "lean_uint64_to_uint16"]
 def UInt64.toUInt16 (a : UInt64) : UInt16 := a.toNat.toUInt16
-@[extern c inline "((uint32_t)#1)"]
+@[extern "lean_uint64_to_uint32"]
 def UInt64.toUInt32 (a : UInt64) : UInt32 := a.toNat.toUInt32
-@[extern c inline "((uint64_t)#1)"]
+@[extern "lean_uint8_to_uint64"]
 def UInt8.toUInt64 (a : UInt8) : UInt64 := a.toNat.toUInt64
-@[extern c inline "((uint64_t)#1)"]
+@[extern "lean_uint16_to_uint64"]
 def UInt16.toUInt64 (a : UInt16) : UInt64 := a.toNat.toUInt64
-@[extern c inline "((uint64_t)#1)"]
+@[extern "lean_uint32_to_uint64"]
 def UInt32.toUInt64 (a : UInt32) : UInt64 := a.toNat.toUInt64
 
 instance : OfNat UInt64 n   := ⟨UInt64.ofNat n⟩
@@ -250,7 +250,7 @@ instance : Div UInt64       := ⟨UInt64.div⟩
 instance : LT UInt64        := ⟨UInt64.lt⟩
 instance : LE UInt64        := ⟨UInt64.le⟩
 
-@[extern c inline "~ #1"]
+@[extern "lean_uint64_complement"]
 def UInt64.complement (a:UInt64) : UInt64 := 0-(a+1)
 
 instance : Complement UInt64 := ⟨UInt64.complement⟩
@@ -260,17 +260,17 @@ instance : Xor UInt64       := ⟨UInt64.xor⟩
 instance : ShiftLeft UInt64  := ⟨UInt64.shiftLeft⟩
 instance : ShiftRight UInt64 := ⟨UInt64.shiftRight⟩
 
-@[extern c inline "(uint64_t)#1"]
+@[extern "lean_bool_to_uint64"]
 def Bool.toUInt64 (b : Bool) : UInt64 := if b then 1 else 0
 
 set_option bootstrap.genMatcherCode false in
-@[extern c inline "#1 < #2"]
+@[extern "lean_uint64_dec_lt"]
 def UInt64.decLt (a b : UInt64) : Decidable (a < b) :=
   match a, b with
   | ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (n < m))
 
 set_option bootstrap.genMatcherCode false in
-@[extern c inline "#1 <= #2"]
+@[extern "lean_uint64_dec_le"]
 def UInt64.decLe (a b : UInt64) : Decidable (a ≤ b) :=
   match a, b with
   | ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (n <= m))
@@ -286,31 +286,31 @@ def USize.ofNat (n : @& Nat) : USize := ⟨Fin.ofNat' n usize_size_gt_zero⟩
 abbrev Nat.toUSize := USize.ofNat
 @[extern "lean_usize_to_nat"]
 def USize.toNat (n : USize) : Nat := n.val.val
-@[extern c inline "#1 + #2"]
+@[extern "lean_usize_add"]
 def USize.add (a b : USize) : USize := ⟨a.val + b.val⟩
-@[extern c inline "#1 - #2"]
+@[extern "lean_usize_sub"]
 def USize.sub (a b : USize) : USize := ⟨a.val - b.val⟩
-@[extern c inline "#1 * #2"]
+@[extern "lean_usize_mul"]
 def USize.mul (a b : USize) : USize := ⟨a.val * b.val⟩
-@[extern c inline "#2 == 0 ? 0 : #1 / #2"]
+@[extern "lean_usize_div"]
 def USize.div (a b : USize) : USize := ⟨a.val / b.val⟩
-@[extern c inline "#2 == 0 ? #1 : #1 % #2"]
+@[extern "lean_usize_mod"]
 def USize.mod (a b : USize) : USize := ⟨a.val % b.val⟩
 @[extern "lean_usize_modn"]
 def USize.modn (a : USize) (n : @& Nat) : USize := ⟨a.val % n⟩
-@[extern c inline "#1 & #2"]
+@[extern "lean_usize_land"]
 def USize.land (a b : USize) : USize := ⟨Fin.land a.val b.val⟩
-@[extern c inline "#1 | #2"]
+@[extern "lean_usize_lor"]
 def USize.lor (a b : USize) : USize := ⟨Fin.lor a.val b.val⟩
-@[extern c inline "#1 ^ #2"]
+@[extern "lean_usize_xor"]
 def USize.xor (a b : USize) : USize := ⟨Fin.xor a.val b.val⟩
-@[extern c inline "#1 << #2 % (sizeof(size_t) * 8)"]
+@[extern "lean_usize_shift_left"]
 def USize.shiftLeft (a b : USize) : USize := ⟨a.val <<< (modn b System.Platform.numBits).val⟩
-@[extern c inline "#1 >> #2 % (sizeof(size_t) * 8)"]
+@[extern "lean_usize_shift_right"]
 def USize.shiftRight (a b : USize) : USize := ⟨a.val >>> (modn b System.Platform.numBits).val⟩
-@[extern c inline "#1"]
+@[extern "lean_uint32_to_usize"]
 def UInt32.toUSize (a : UInt32) : USize := a.toNat.toUSize
-@[extern c inline "(uint32_t)#1"]
+@[extern "lean_usize_to_uint32"]
 def USize.toUInt32 (a : USize) : UInt32 := a.toNat.toUInt32
 
 def USize.lt (a b : USize) : Prop := a.val < b.val
@@ -326,7 +326,7 @@ instance : Div USize       := ⟨USize.div⟩
 instance : LT USize        := ⟨USize.lt⟩
 instance : LE USize        := ⟨USize.le⟩
 
-@[extern c inline "~ #1"]
+@[extern "lean_usize_complement"]
 def USize.complement (a:USize) : USize := 0-(a+1)
 
 instance : Complement USize := ⟨USize.complement⟩
@@ -337,13 +337,13 @@ instance : ShiftLeft USize  := ⟨USize.shiftLeft⟩
 instance : ShiftRight USize := ⟨USize.shiftRight⟩
 
 set_option bootstrap.genMatcherCode false in
-@[extern c inline "#1 < #2"]
+@[extern "lean_usize_dec_lt"]
 def USize.decLt (a b : USize) : Decidable (a < b) :=
   match a, b with
   | ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (n < m))
 
 set_option bootstrap.genMatcherCode false in
-@[extern c inline "#1 <= #2"]
+@[extern "lean_usize_dec_le"]
 def USize.decLe (a b : USize) : Decidable (a ≤ b) :=
   match a, b with
   | ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (n <= m))
diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index f53b6093a6..8920c72469 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -811,7 +811,7 @@ def UInt8.ofNatCore (n : @& Nat) (h : LT.lt n UInt8.size) : UInt8 := {
 }
 
 set_option bootstrap.genMatcherCode false in
-@[extern c inline "#1 == #2"]
+@[extern "lean_uint8_dec_eq"]
 def UInt8.decEq (a b : UInt8) : Decidable (Eq a b) :=
   match a, b with
   | ⟨n⟩, ⟨m⟩ =>
@@ -835,7 +835,7 @@ def UInt16.ofNatCore (n : @& Nat) (h : LT.lt n UInt16.size) : UInt16 := {
 }
 
 set_option bootstrap.genMatcherCode false in
-@[extern c inline "#1 == #2"]
+@[extern "lean_uint16_dec_eq"]
 def UInt16.decEq (a b : UInt16) : Decidable (Eq a b) :=
   match a, b with
   | ⟨n⟩, ⟨m⟩ =>
@@ -862,7 +862,7 @@ def UInt32.ofNatCore (n : @& Nat) (h : LT.lt n UInt32.size) : UInt32 := {
 def UInt32.toNat (n : UInt32) : Nat := n.val.val
 
 set_option bootstrap.genMatcherCode false in
-@[extern c inline "#1 == #2"]
+@[extern "lean_uint32_dec_eq"]
 def UInt32.decEq (a b : UInt32) : Decidable (Eq a b) :=
   match a, b with
   | ⟨n⟩, ⟨m⟩ =>
@@ -880,13 +880,13 @@ instance : LE UInt32 where
   le a b := LE.le a.val b.val
 
 set_option bootstrap.genMatcherCode false in
-@[extern c inline "#1 < #2"]
+@[extern "lean_uint32_dec_lt"]
 def UInt32.decLt (a b : UInt32) : Decidable (LT.lt a b) :=
   match a, b with
   | ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (LT.lt n m))
 
 set_option bootstrap.genMatcherCode false in
-@[extern c inline "#1 <= #2"]
+@[extern "lean_uint32_dec_le"]
 def UInt32.decLe (a b : UInt32) : Decidable (LE.le a b) :=
   match a, b with
   | ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (LE.le n m))
@@ -907,7 +907,7 @@ def UInt64.ofNatCore (n : @& Nat) (h : LT.lt n UInt64.size) : UInt64 := {
 }
 
 set_option bootstrap.genMatcherCode false in
-@[extern c inline "#1 == #2"]
+@[extern c "lean_uint64_dec_eq"]
 def UInt64.decEq (a b : UInt64) : Decidable (Eq a b) :=
   match a, b with
   | ⟨n⟩, ⟨m⟩ =>
@@ -938,7 +938,7 @@ def USize.ofNatCore (n : @& Nat) (h : LT.lt n USize.size) : USize := {
 }
 
 set_option bootstrap.genMatcherCode false in
-@[extern c inline "#1 == #2"]
+@[extern c "lean_usize_dec_eq"]
 def USize.decEq (a b : USize) : Decidable (Eq a b) :=
   match a, b with
   | ⟨n⟩, ⟨m⟩ =>
@@ -1644,10 +1644,10 @@ class Hashable (α : Sort u) where
 
 export Hashable (hash)
 
-@[extern c inline "(size_t)#1"]
+@[extern c "lean_uint64_to_usize"]
 constant UInt64.toUSize (u : UInt64) : USize
 
-@[extern c inline "(uint64_t)#1"]
+@[extern c "lean_usize_to_uint64"]
 constant USize.toUInt64 (u : USize) : UInt64
 
 @[extern "lean_uint64_mix_hash"]
diff --git a/src/include/lean/lean.h b/src/include/lean/lean.h
index 081726de6c..474a8be47a 100644
--- a/src/include/lean/lean.h
+++ b/src/include/lean/lean.h
@@ -1476,6 +1476,10 @@ static inline uint8_t lean_int_dec_nonneg(b_lean_obj_arg a) {
         return lean_int_big_nonneg(a);
 }
 
+/* Bool */
+
+static inline uint64_t lean_bool_to_uint64(uint8_t a) { return ((uint64_t)a); }
+
 
 /* UInt8 */
 
@@ -1489,6 +1493,12 @@ static inline uint8_t lean_uint8_sub(uint8_t a1, uint8_t a2) { return a1-a2; }
 static inline uint8_t lean_uint8_mul(uint8_t a1, uint8_t a2) { return a1*a2; }
 static inline uint8_t lean_uint8_div(uint8_t a1, uint8_t a2) { return a2 == 0 ? 0  : a1/a2; }
 static inline uint8_t lean_uint8_mod(uint8_t a1, uint8_t a2) { return a2 == 0 ? a1 : a1%a2; }
+static inline uint8_t lean_uint8_land(uint8_t a, uint8_t b) { return a & b; }
+static inline uint8_t lean_uint8_lor(uint8_t a, uint8_t b) { return a | b; }
+static inline uint8_t lean_uint8_xor(uint8_t a, uint8_t b) { return a ^ b; }
+static inline uint8_t lean_uint8_shift_left(uint8_t a, uint8_t b) { return a << (b % 8); }
+static inline uint8_t lean_uint8_shift_right(uint8_t a, uint8_t b) { return a >> (b % 8); }
+static inline uint8_t lean_uint8_complement(uint8_t a) { return ~a; }
 static inline uint8_t lean_uint8_modn(uint8_t a1, b_lean_obj_arg a2) {
     if (LEAN_LIKELY(lean_is_scalar(a2))) {
         unsigned n2 = lean_unbox(a2);
@@ -1501,6 +1511,12 @@ static inline uint8_t lean_uint8_dec_eq(uint8_t a1, uint8_t a2) { return a1 == a
 static inline uint8_t lean_uint8_dec_lt(uint8_t a1, uint8_t a2) { return a1 < a2; }
 static inline uint8_t lean_uint8_dec_le(uint8_t a1, uint8_t a2) { return a1 <= a2; }
 
+
+/* Unit8 -> other */
+static inline uint16_t lean_uint8_to_uint16(uint8_t a) { return ((uint16_t)a); }
+static inline uint32_t lean_uint8_to_uint32(uint8_t a) { return ((uint32_t)a); }
+static inline uint64_t lean_uint8_to_uint64(uint8_t a) { return ((uint64_t)a); }
+
 /* UInt16 */
 
 LEAN_SHARED uint16_t lean_uint16_of_big_nat(b_lean_obj_arg a);
@@ -1513,6 +1529,12 @@ static inline uint16_t lean_uint16_sub(uint16_t a1, uint16_t a2) { return a1-a2;
 static inline uint16_t lean_uint16_mul(uint16_t a1, uint16_t a2) { return a1*a2; }
 static inline uint16_t lean_uint16_div(uint16_t a1, uint16_t a2) { return a2 == 0 ? 0  : a1/a2; }
 static inline uint16_t lean_uint16_mod(uint16_t a1, uint16_t a2) { return a2 == 0 ? a1 : a1%a2; }
+static inline uint16_t lean_uint16_land(uint16_t a, uint16_t b) { return a & b; }
+static inline uint16_t lean_uint16_lor(uint16_t a, uint16_t b) { return a | b; }
+static inline uint16_t lean_uint16_xor(uint16_t a, uint16_t b) { return a ^ b; }
+static inline uint16_t lean_uint16_shift_left(uint16_t a, uint16_t b) { return a << (b % 16); }
+static inline uint16_t lean_uint16_shift_right(uint16_t a, uint16_t b) { return a >> (b % 16); }
+static inline uint16_t lean_uint16_complement(uint16_t a) { return ~a; }
 static inline uint16_t lean_uint16_modn(uint16_t a1, b_lean_obj_arg a2) {
     if (LEAN_LIKELY(lean_is_scalar(a2))) {
         unsigned n2 = lean_unbox(a2);
@@ -1525,6 +1547,11 @@ static inline uint8_t lean_uint16_dec_eq(uint16_t a1, uint16_t a2) { return a1 =
 static inline uint8_t lean_uint16_dec_lt(uint16_t a1, uint16_t a2) { return a1 < a2; }
 static inline uint8_t lean_uint16_dec_le(uint16_t a1, uint16_t a2) { return a1 <= a2; }
 
+/*uint16 -> other */
+static inline uint8_t lean_uint16_to_uint8(uint16_t a) { return ((uint8_t)a); }
+static inline uint32_t lean_uint16_to_uint32(uint16_t a) { return ((uint32_t)a); }
+static inline uint64_t lean_uint16_to_uint64(uint16_t a) { return ((uint64_t)a); }
+
 /* UInt32 */
 
 LEAN_SHARED uint32_t lean_uint32_of_big_nat(b_lean_obj_arg a);
@@ -1537,6 +1564,12 @@ static inline uint32_t lean_uint32_sub(uint32_t a1, uint32_t a2) { return a1-a2;
 static inline uint32_t lean_uint32_mul(uint32_t a1, uint32_t a2) { return a1*a2; }
 static inline uint32_t lean_uint32_div(uint32_t a1, uint32_t a2) { return a2 == 0 ? 0  : a1/a2; }
 static inline uint32_t lean_uint32_mod(uint32_t a1, uint32_t a2) { return a2 == 0 ? a1 : a1%a2; }
+static inline uint32_t lean_uint32_land(uint32_t a, uint32_t b) { return a & b; }
+static inline uint32_t lean_uint32_lor(uint32_t a, uint32_t b) { return a | b; }
+static inline uint32_t lean_uint32_xor(uint32_t a, uint32_t b) { return a ^ b; }
+static inline uint32_t lean_uint32_shift_left(uint32_t a, uint32_t b) { return a << (b % 32); }
+static inline uint32_t lean_uint32_shift_right(uint32_t a, uint32_t b) { return a >> (b % 32); }
+static inline uint32_t lean_uint32_complement(uint32_t a) { return ~a; }
 LEAN_SHARED uint32_t lean_uint32_big_modn(uint32_t a1, b_lean_obj_arg a2);
 static inline uint32_t lean_uint32_modn(uint32_t a1, b_lean_obj_arg a2) {
     if (LEAN_LIKELY(lean_is_scalar(a2))) {
@@ -1554,6 +1587,13 @@ static inline uint8_t lean_uint32_dec_eq(uint32_t a1, uint32_t a2) { return a1 =
 static inline uint8_t lean_uint32_dec_lt(uint32_t a1, uint32_t a2) { return a1 < a2; }
 static inline uint8_t lean_uint32_dec_le(uint32_t a1, uint32_t a2) { return a1 <= a2; }
 
+/* uint32 -> other */
+static inline uint8_t lean_uint32_to_uint8(uint32_t a) { return ((uint8_t)a); }
+static inline uint16_t lean_uint32_to_uint16(uint32_t a) { return ((uint16_t)a); }
+static inline uint64_t lean_uint32_to_uint64(uint32_t a) { return ((uint64_t)a); }
+static inline size_t lean_uint32_to_usize(uint32_t a) { return a; }
+
+
 /* UInt64 */
 
 LEAN_SHARED uint64_t lean_uint64_of_big_nat(b_lean_obj_arg a);
@@ -1565,6 +1605,12 @@ static inline uint64_t lean_uint64_sub(uint64_t a1, uint64_t a2) { return a1-a2;
 static inline uint64_t lean_uint64_mul(uint64_t a1, uint64_t a2) { return a1*a2; }
 static inline uint64_t lean_uint64_div(uint64_t a1, uint64_t a2) { return a2 == 0 ? 0  : a1/a2; }
 static inline uint64_t lean_uint64_mod(uint64_t a1, uint64_t a2) { return a2 == 0 ? a1 : a1%a2; }
+static inline uint64_t lean_uint64_land(uint64_t a, uint64_t b) { return a & b; }
+static inline uint64_t lean_uint64_lor(uint64_t a, uint64_t b) { return a | b; }
+static inline uint64_t lean_uint64_xor(uint64_t a, uint64_t b) { return a ^ b; }
+static inline uint64_t lean_uint64_shift_left(uint64_t a, uint64_t b) { return a << (b % 64); }
+static inline uint64_t lean_uint64_shift_right(uint64_t a, uint64_t b) { return a >> (b % 64); }
+static inline uint64_t lean_uint64_complement(uint64_t a) { return ~a; }
 LEAN_SHARED uint64_t lean_uint64_big_modn(uint64_t a1, b_lean_obj_arg a2);
 static inline uint64_t lean_uint64_modn(uint64_t a1, b_lean_obj_arg a2) {
     if (LEAN_LIKELY(lean_is_scalar(a2))) {
@@ -1579,6 +1625,13 @@ static inline uint8_t lean_uint64_dec_lt(uint64_t a1, uint64_t a2) { return a1 <
 static inline uint8_t lean_uint64_dec_le(uint64_t a1, uint64_t a2) { return a1 <= a2; }
 LEAN_SHARED uint64_t lean_uint64_mix_hash(uint64_t a1, uint64_t a2);
 
+
+/* uint64 -> other */
+static inline uint8_t lean_uint64_to_uint8(uint64_t a) { return ((uint8_t)a); }
+static inline uint16_t lean_uint64_to_uint16(uint64_t a) { return ((uint16_t)a); }
+static inline uint32_t lean_uint64_to_uint32(uint64_t a) { return ((uint32_t)a); }
+static inline size_t lean_uint64_to_usize(uint64_t a) { return ((size_t)a); }
+
 /* USize */
 
 LEAN_SHARED size_t lean_usize_of_big_nat(b_lean_obj_arg a);
@@ -1590,6 +1643,12 @@ static inline size_t lean_usize_sub(size_t a1, size_t a2) { return a1-a2; }
 static inline size_t lean_usize_mul(size_t a1, size_t a2) { return a1*a2; }
 static inline size_t lean_usize_div(size_t a1, size_t a2) { return a2 == 0 ? 0  : a1/a2; }
 static inline size_t lean_usize_mod(size_t a1, size_t a2) { return a2 == 0 ? a1 : a1%a2; }
+static inline size_t lean_usize_land(size_t a, size_t b) { return a & b; }
+static inline size_t lean_usize_lor(size_t a, size_t b) { return a | b; }
+static inline size_t lean_usize_xor(size_t a, size_t b) { return a ^ b; }
+static inline size_t lean_usize_shift_left(size_t a, size_t b) { return a << (b %  (sizeof(size_t) * 8)); }
+static inline size_t lean_usize_shift_right(size_t a, size_t b) { return a >> (b % (sizeof(size_t) * 8)); }
+static inline size_t lean_usize_complement(size_t a) { return ~a; }
 LEAN_SHARED size_t lean_usize_big_modn(size_t a1, b_lean_obj_arg a2);
 static inline size_t lean_usize_modn(size_t a1, b_lean_obj_arg a2) {
     if (LEAN_LIKELY(lean_is_scalar(a2))) {
@@ -1604,6 +1663,12 @@ static inline uint8_t lean_usize_dec_lt(size_t a1, size_t a2) { return a1 < a2;
 static inline uint8_t lean_usize_dec_le(size_t a1, size_t a2) { return a1 <= a2; }
 LEAN_SHARED size_t lean_usize_mix_hash(size_t a1, size_t a2);
 
+
+
+/* usize -> other */
+static inline uint32_t lean_usize_to_uint32(size_t a) { return ((uint32_t)a); }
+static inline uint64_t lean_usize_to_uint64(size_t a) { return ((uint64_t)a); }
+
 /* Float */
 
 LEAN_SHARED double lean_float_of_nat(b_lean_obj_arg a);
@@ -1745,6 +1810,21 @@ static inline uint64_t lean_name_hash(b_lean_obj_arg n) {
         return lean_name_hash_ptr(n);
 }
 
+/* float primitives */
+ static inline uint8_t lean_float_to_uint8(double a) { return (uint8_t)a; }
+ static inline uint16_t lean_float_to_uint16(double a) { return (uint16_t)a; }
+ static inline uint32_t lean_float_to_uint32(double a) { return (uint32_t)a; }
+ static inline uint64_t lean_float_to_uint64(double a) { return (uint64_t)a; }
+ static inline size_t lean_float_to_usize(double a) { return (size_t)a; }
+ static inline double lean_float_add(double a, double b) { return a + b; }
+ static inline double lean_float_sub(double a, double b) { return a - b; }
+ static inline double lean_float_mul(double a, double b) { return a * b; }
+ static inline double lean_float_div(double a, double b) { return a / b; }
+ static inline double lean_float_negate(double a) { return -a; }
+ static inline uint8_t lean_float_beq(double a, double b) { return a == b; }
+ static inline uint8_t lean_float_decLe(double a, double b) { return a <= b; }
+ static inline uint8_t lean_float_decLt(double a, double b) { return a < b; }
+
 #ifdef __cplusplus
 }
 #endif