diff --git a/library/init/lean/compiler/constfolding.lean b/library/init/lean/compiler/constfolding.lean
index 7bfc5d6d5b..11ed4e86f8 100644
--- a/library/init/lean/compiler/constfolding.lean
+++ b/library/init/lean/compiler/constfolding.lean
@@ -15,12 +15,12 @@ namespace Compiler
 def BinFoldFn := Bool → Expr → Expr → Option Expr
 def UnFoldFn  := Bool → Expr → Option Expr
 
-def mkUintTypeName (nbytes : Nat) : Name :=
+def mkUIntTypeName (nbytes : Nat) : Name :=
 mkSimpleName ("UInt" ++ toString nbytes)
 
 structure NumScalarTypeInfo :=
 (nbits : Nat)
-(id : Name        := mkUintTypeName nbits)
+(id : Name        := mkUIntTypeName nbits)
 (ofNatFn : Name := Name.mkString id "ofNat")
 (size : Nat       := 2^nbits)
 
@@ -53,24 +53,24 @@ Expr.app (Expr.const info.ofNatFn []) (Expr.lit (Literal.natVal (n%info.size)))
 def mkUInt32Lit (n : Nat) : Expr :=
 mkUIntLit {nbits := 32} n
 
-def foldBinUint (fn : NumScalarTypeInfo → Bool → Nat → Nat → Nat) (beforeErasure : Bool) (a₁ a₂ : Expr) : Option Expr :=
+def foldBinUInt (fn : NumScalarTypeInfo → Bool → Nat → Nat → Nat) (beforeErasure : Bool) (a₁ a₂ : Expr) : Option Expr :=
 do n₁   ← getNumLit a₁,
    n₂   ← getNumLit a₂,
    info ← getInfoFromVal a₁,
    pure $ mkUIntLit info (fn info beforeErasure n₁ n₂)
 
-def foldUintAdd := foldBinUint $ λ _ _, (+)
-def foldUintMul := foldBinUint $ λ _ _, (*)
-def foldUintDiv := foldBinUint $ λ _ _, (/)
-def foldUintMod := foldBinUint $ λ _ _, (%)
-def foldUintSub := foldBinUint $ λ info _ a b, (a + (info.size - b))
+def foldUIntAdd := foldBinUInt $ λ _ _, (+)
+def foldUIntMul := foldBinUInt $ λ _ _, (*)
+def foldUIntDiv := foldBinUInt $ λ _ _, (/)
+def foldUIntMod := foldBinUInt $ λ _ _, (%)
+def foldUIntSub := foldBinUInt $ λ info _ a b, (a + (info.size - b))
 
-def preUintBinFoldFns : List (Name × BinFoldFn) :=
-[(`add, foldUintAdd), (`mul, foldUintMul), (`div, foldUintDiv),
- (`mod, foldUintMod), (`sub, foldUintSub)]
+def preUIntBinFoldFns : List (Name × BinFoldFn) :=
+[(`add, foldUIntAdd), (`mul, foldUIntMul), (`div, foldUIntDiv),
+ (`mod, foldUIntMod), (`sub, foldUIntSub)]
 
 def uintBinFoldFns : List (Name × BinFoldFn) :=
-numScalarTypes.foldl (λ r info, r ++ (preUintBinFoldFns.map (λ ⟨suffix, fn⟩, (info.id ++ suffix, fn)))) []
+numScalarTypes.foldl (λ r info, r ++ (preUIntBinFoldFns.map (λ ⟨suffix, fn⟩, (info.id ++ suffix, fn)))) []
 
 def foldNatBinOp (fn : Nat → Nat → Nat) (a₁ a₂ : Expr) : Option Expr :=
 do n₁   ← getNumLit a₁,
diff --git a/library/init/lean/compiler/ir.lean b/library/init/lean/compiler/ir.lean
index 0a5d1dbbc8..4fb3a8f0f2 100644
--- a/library/init/lean/compiler/ir.lean
+++ b/library/init/lean/compiler/ir.lean
@@ -42,15 +42,15 @@ first need to test whether the `tobject` is really a pointer or not.
 Remark: the Lean runtime assumes that sizeof(void*) == sizeof(sizeT).
 Lean cannot be compiled on old platforms where this is not True. -/
 inductive IRType
-| float | Uint8 | Uint16 | Uint32 | Uint64 | Usize
+| float | uint8 | uint16 | uint32 | uint64 | Usize
 | irrelevant | object | tobject
 
 def IRType.beq : IRType → IRType → Bool
 | IRType.float      IRType.float      := true
-| IRType.Uint8      IRType.Uint8      := true
-| IRType.Uint16     IRType.Uint16     := true
-| IRType.Uint32     IRType.Uint32     := true
-| IRType.Uint64     IRType.Uint64     := true
+| IRType.uint8      IRType.uint8      := true
+| IRType.uint16     IRType.uint16     := true
+| IRType.uint32     IRType.uint32     := true
+| IRType.uint64     IRType.uint64     := true
 | IRType.Usize      IRType.Usize      := true
 | IRType.irrelevant IRType.irrelevant := true
 | IRType.object     IRType.object     := true
@@ -120,9 +120,9 @@ inductive Expr
 /- Given `x : [t]object`, obtain the scalar value. -/
 | unbox (x : varid)
 | lit (v : Litval)
-/- Return `1 : Uint8` Iff `RC(x) > 1` -/
+/- Return `1 : uint8` Iff `RC(x) > 1` -/
 | isShared (x : varid)
-/- Return `1 : Uint8` Iff `x : tobject` is a tagged pointer (storing a scalar value). -/
+/- Return `1 : uint8` Iff `x : tobject` is a tagged pointer (storing a scalar value). -/
 | isTaggedPtr (x : varid)
 
 structure Param :=