diff --git a/library/init/coe.lean b/library/init/coe.lean
index 863dd3f704..f7ab1fde84 100644
--- a/library/init/coe.lean
+++ b/library/init/coe.lean
@@ -144,7 +144,7 @@ instance coeToLift {a : Sort u} {b : Sort v} [HasCoeT a b] : HasLiftT a b :=
 /- basic coercions -/
 
 instance coeBoolToProp : HasCoe Bool Prop :=
-⟨λ y, y = tt⟩
+⟨λ y, y = true⟩
 
 /- Tactics such as the simplifier only unfold reducible constants when checking whether two terms are definitionally
    equal or a Term is a proposition. The motivation is performance.
@@ -152,10 +152,10 @@ instance coeBoolToProp : HasCoe Bool Prop :=
    Thus, we mark the following instance as @[reducible], otherwise `simp` will not visit `↑p` when simplifying `↑p -> q`.
 -/
 @[reducible] instance coeSortBool : HasCoeToSort Bool :=
-⟨Prop, λ y, y = tt⟩
+⟨Prop, λ y, y = true⟩
 
 instance coeDecidableEq (x : Bool) : Decidable (coe x) :=
-show Decidable (x = tt), from decEq x tt
+show Decidable (x = true), from decEq x true
 
 instance coeSubtype {a : Sort u} {p : a → Prop} : HasCoe {x // p x} a :=
 ⟨Subtype.val⟩
diff --git a/library/init/control/alternative.lean b/library/init/control/alternative.lean
index 77db41eb51..d499ecd977 100644
--- a/library/init/control/alternative.lean
+++ b/library/init/control/alternative.lean
@@ -30,8 +30,8 @@ if h : p then pure ⟨h⟩ else failure
 /- Later we define a coercion from Bool to Prop, but this version will still be useful.
    Given (t : tactic Bool), we can write t >>= guardb -/
 @[inline] def guardb {f : Type → Type v} [Alternative f] : Bool → f Unit
-| tt := pure ()
-| ff := failure
+| true  := pure ()
+| false := failure
 
 @[inline] def optional (x : f α) : f (Option α) :=
 some <$> x <|> pure none
diff --git a/library/init/control/combinators.lean b/library/init/control/combinators.lean
index b0d8ac3d75..0f5d620a3f 100644
--- a/library/init/control/combinators.lean
+++ b/library/init/control/combinators.lean
@@ -56,13 +56,13 @@ def List.mfirst {m : Type u → Type v} [Monad m] [Alternative m] {α : Type w}
 
 @[specialize]
 def List.mexists {m : Type → Type u} [Monad m] {α : Type v} (f : α → m Bool) : List α → m Bool
-| []      := pure ff
-| (a::as) := do b ← f a, if b then pure tt else List.mexists as
+| []      := pure false
+| (a::as) := do b ← f a, if b then pure true else List.mexists as
 
 @[specialize]
 def List.mforall {m : Type → Type u} [Monad m] {α : Type v} (f : α → m Bool) : List α → m Bool
-| []      := pure tt
-| (a::as) := do b ← f a, if b then List.mforall as else pure ff
+| []      := pure true
+| (a::as) := do b ← f a, if b then List.mforall as else pure false
 
 @[macroInline] def when {m : Type → Type u} [Monad m] (c : Prop) [h : Decidable c] (t : m Unit) : m Unit :=
 if c then t else pure ()
diff --git a/library/init/control/estate.lean b/library/init/control/estate.lean
index 070ebc3c18..58a0ec130f 100644
--- a/library/init/control/estate.lean
+++ b/library/init/control/estate.lean
@@ -94,7 +94,7 @@ instance [Inhabited ε] : Inhabited (Estate ε σ α) :=
 
 /-- Alternative orelse operator that allows to select which exception should be used.
     The default is to use the first exception since the standard `orelse` uses the second. -/
-@[inline] protected def orelse' (x₁ x₂ : Estate ε σ α) (useFirstEx := tt) : Estate ε σ α :=
+@[inline] protected def orelse' (x₁ x₂ : Estate ε σ α) (useFirstEx := true) : Estate ε σ α :=
 λ r, match x₁ r with
      | Result.error e₁ s₁ :=
        (match x₂ (resultOk.mk ⟨⟩ s₁) with
diff --git a/library/init/control/except.lean b/library/init/control/except.lean
index df13d5f4eb..01aaf48000 100644
--- a/library/init/control/except.lean
+++ b/library/init/control/except.lean
@@ -55,8 +55,8 @@ match ma with
 | (Except.ok v) := f v
 
 @[inline] protected def toBool {α : Type v} : Except ε α → Bool
-| (Except.ok _)    := tt
-| (Except.error _) := ff
+| (Except.ok _)    := true
+| (Except.error _) := false
 
 @[inline] protected def toOption {α : Type v} : Except ε α → Option α
 | (Except.ok a)    := some a
@@ -130,7 +130,7 @@ catch t₁ $ λ _, t₂
 
 /-- Alternative orelse operator that allows to select which exception should be used.
     The default is to use the first exception since the standard `orelse` uses the second. -/
-@[inline] def orelse' [MonadExcept ε m] {α : Type v} (t₁ t₂ : m α) (useFirstEx := tt) : m α :=
+@[inline] def orelse' [MonadExcept ε m] {α : Type v} (t₁ t₂ : m α) (useFirstEx := true) : m α :=
 catch t₁ $ λ e₁, catch t₂ $ λ e₂, throw (if useFirstEx then e₁ else e₂)
 
 @[inline] def liftExcept {ε' : Type u} [MonadExcept ε m] [HasLiftT ε' ε] [Monad m] {α : Type v} : Except ε' α → m α
diff --git a/library/init/core.lean b/library/init/core.lean
index 103b33b325..8f919de323 100644
--- a/library/init/core.lean
+++ b/library/init/core.lean
@@ -286,8 +286,8 @@ structure Psigma {α : Sort u} (β : α → Sort v) :=
 mk :: (fst : α) (snd : β fst)
 
 inductive Bool : Type
-| ff : Bool
-| tt : Bool
+| false : Bool
+| true : Bool
 
 /- Remark: Subtype must take a Sort instead of Type because of the axiom strongIndefiniteDescription. -/
 structure Subtype {α : Sort u} (p : α → Prop) :=
@@ -321,7 +321,7 @@ inductive Option (α : Type u)
 | some (val : α) : Option
 
 export Option (none some)
-export Bool (ff tt)
+export Bool (false true)
 
 inductive List (T : Type u)
 | nil {} : List
@@ -337,7 +337,7 @@ inductive Nat
 /- Auxiliary axiom used to implement `sorry`.
    TODO: add this theorem on-demand. That is,
    we should only add it if after the first error. -/
-unsafe axiom sorryAx (α : Sort u) (synthetic := tt) : α
+unsafe axiom sorryAx (α : Sort u) (synthetic := true) : α
 
 /- Declare builtin and reserved notation -/
 
@@ -603,25 +603,25 @@ attribute [elabSimple] BinTree.Node BinTree.leaf
 /- Boolean operators -/
 
 @[macroInline] def cond {a : Type u} : Bool → a → a → a
-| tt x y := x
-| ff x y := y
+| true  x y := x
+| false x y := y
 
 @[macroInline] def bor : Bool → Bool → Bool
-| tt _  := tt
-| ff b  := b
+| true  _  := true
+| false b  := b
 
 @[macroInline] def band : Bool → Bool → Bool
-| ff _  := ff
-| tt b  := b
+| false _  := false
+| true  b  := b
 
 @[macroInline] def bnot : Bool → Bool
-| tt := ff
-| ff := tt
+| true  := false
+| false := true
 
 @[macroInline] def bxor : Bool → Bool → Bool
-| tt ff  := tt
-| ff tt  := tt
-| _  _   := ff
+| true  false := true
+| false true  := true
+| _  _        := false
 
 prefix ! := bnot
 infix || := bor
@@ -721,13 +721,13 @@ theorem trueNeFalse : ¬True = False :=
 neFalseOfSelf trivial
 end ne
 
-theorem eqFfOfNeTt : ∀ {b : Bool}, b ≠ tt → b = ff
-| tt h := False.elim (h rfl)
-| ff h := rfl
+theorem eqFfOfNeTt : ∀ {b : Bool}, b ≠ true → b = false
+| true h := False.elim (h rfl)
+| false h := rfl
 
-theorem eqTtOfNeFf : ∀ {b : Bool}, b ≠ ff → b = tt
-| tt h := rfl
-| ff h := False.elim (h rfl)
+theorem eqTtOfNeFf : ∀ {b : Bool}, b ≠ false → b = true
+| true h := rfl
+| false h := False.elim (h rfl)
 
 section
 variables {α β φ : Sort u} {a a' : α} {b b' : β} {c : φ}
@@ -1086,14 +1086,14 @@ theorem forallNotOfNotExists {α : Sort u} {p : α → Prop} : ¬(∃ x, p x) 
 /- Decidable -/
 
 @[macroInline] def Decidable.toBool (p : Prop) [h : Decidable p] : Bool :=
-Decidable.casesOn h (λ h₁, Bool.ff) (λ h₂, Bool.tt)
+Decidable.casesOn h (λ h₁, false) (λ h₂, true)
 
 export Decidable (isTrue isFalse toBool)
 
-theorem toBoolTrueEqTt (h : Decidable True) : @toBool True h = tt :=
+theorem toBoolTrueEqTt (h : Decidable True) : @toBool True h = true :=
 Decidable.casesOn h (λ h, False.elim (Iff.mp notTrue h)) (λ _, rfl)
 
-theorem toBoolFalseEqFf (h : Decidable False) : @toBool False h = ff :=
+theorem toBoolFalseEqFf (h : Decidable False) : @toBool False h = false :=
 Decidable.casesOn h (λ h, rfl) (λ h, False.elim h)
 
 instance : Decidable True :=
@@ -1230,24 +1230,24 @@ match decEq a b with
 | isTrue h := isFalse $ λ h', absurd h h'
 | isFalse h := isTrue h
 
-theorem Bool.ffNeTt (h : ff = tt) : False :=
+theorem Bool.falseNeTrue (h : false = true) : False :=
 Bool.noConfusion h
 
-def isDecEq {α : Sort u} (p : α → α → Bool) : Prop   := ∀ ⦃x y : α⦄, p x y = tt → x = y
-def isDecRefl {α : Sort u} (p : α → α → Bool) : Prop := ∀ x, p x x = tt
+def isDecEq {α : Sort u} (p : α → α → Bool) : Prop   := ∀ ⦃x y : α⦄, p x y = true → x = y
+def isDecRefl {α : Sort u} (p : α → α → Bool) : Prop := ∀ x, p x x = true
 
 instance : DecidableEq Bool :=
 {decEq := λ a b, match a, b with
- | ff, ff := isTrue rfl
- | ff, tt := isFalse Bool.ffNeTt
- | tt, ff := isFalse (ne.symm Bool.ffNeTt)
- | tt, tt := isTrue rfl}
+ | false, false := isTrue rfl
+ | false, true  := isFalse Bool.falseNeTrue
+ | true, false  := isFalse (ne.symm Bool.falseNeTrue)
+ | true, true   := isTrue rfl}
 
 @[inline]
 def decidableEqOfBoolPred {α : Sort u} {p : α → α → Bool} (h₁ : isDecEq p) (h₂ : isDecRefl p) : DecidableEq α :=
 {decEq := λ x y : α,
- if hp : p x y = tt then isTrue (h₁ hp)
- else isFalse (assume hxy : x = y, absurd (h₂ y) (@Eq.recOn _ _ (λ z _, ¬p z y = tt) _ hxy hp))}
+ if hp : p x y = true then isTrue (h₁ hp)
+ else isFalse (assume hxy : x = y, absurd (h₂ y) (@Eq.recOn _ _ (λ z _, ¬p z y = true) _ hxy hp))}
 
 theorem decidableEqInlRefl {α : Sort u} [DecidableEq α] (a : α) : decEq a a = isTrue (Eq.refl a) :=
 match (decEq a a) with
@@ -1414,7 +1414,7 @@ Inhabited.casesOn h (λ b, ⟨λ a, b⟩)
 instance pi.Inhabited (α : Sort u) {β : α → Sort v} [Π x, Inhabited (β x)] : Inhabited (Π x, β x) :=
 ⟨λ a, default (β a)⟩
 
-instance : Inhabited Bool := ⟨ff⟩
+instance : Inhabited Bool := ⟨false⟩
 
 instance : Inhabited True := ⟨trivial⟩
 
diff --git a/library/init/data/list/basic.lean b/library/init/data/list/basic.lean
index f5c4cfafd2..b65d8872d2 100644
--- a/library/init/data/list/basic.lean
+++ b/library/init/data/list/basic.lean
@@ -119,9 +119,9 @@ def lengthAux : List α → Nat → Nat
 def length (as : List α) : Nat :=
 lengthAux as 0
 
-def Empty : List α → Bool
-| []       := tt
-| (_ :: _) := ff
+def empty : List α → Bool
+| []       := true
+| (_ :: _) := false
 
 open Option Nat
 
@@ -226,10 +226,10 @@ def take : ℕ → List α → List α
 | (a :: l) := some $ foldr1 f (a :: l) (λ Eq, List.noConfusion Eq)
 
 @[inline] def any (l : List α) (p : α → Bool) : Bool :=
-foldr (λ a r, p a || r) ff l
+foldr (λ a r, p a || r) false l
 
 @[inline] def all (l : List α) (p : α → Bool) : Bool :=
-foldr (λ a r, p a && r) tt l
+foldr (λ a r, p a && r) true l
 
 def bor  (l : List Bool) : Bool := any l id
 
@@ -355,13 +355,13 @@ lemma ltEqNotGe [HasLt α] [decidableRel ((<) : α → α → Prop)] : ∀ l₁
   show (l₁ < l₂) = ¬ ¬ (l₁ < l₂), from
   Eq.subst (propext (notNotIff (l₁ < l₂))).symm rfl
 
-/--  `isPrefixOf l₁ l₂` returns `tt` Iff `l₁` is a prefix of `l₂`. -/
+/--  `isPrefixOf l₁ l₂` returns `true` Iff `l₁` is a prefix of `l₂`. -/
 def isPrefixOf [DecidableEq α] : List α → List α → Bool
-| []      _       := tt
-| _       []      := ff
+| []      _       := true
+| _       []      := false
 | (a::as) (b::bs) := toBool (a = b) && isPrefixOf as bs
 
-/--  `isSuffixOf l₁ l₂` returns `tt` Iff `l₁` is a suffix of `l₂`. -/
+/--  `isSuffixOf l₁ l₂` returns `true` Iff `l₁` is a suffix of `l₂`. -/
 def isSuffixOf [DecidableEq α] (l₁ l₂ : List α) : Bool :=
 isPrefixOf l₁.reverse l₂.reverse
 
diff --git a/library/init/data/nat/basic.lean b/library/init/data/nat/basic.lean
index 832d4100af..6177503a60 100644
--- a/library/init/data/nat/basic.lean
+++ b/library/init/data/nat/basic.lean
@@ -13,32 +13,32 @@ namespace Nat
 
 @[extern cpp "lean::nat_dec_eq"]
 def beq : Nat → Nat → Bool
-| zero     zero     := tt
-| zero     (succ m) := ff
-| (succ n) zero     := ff
+| zero     zero     := true
+| zero     (succ m) := false
+| (succ n) zero     := false
 | (succ n) (succ m) := beq n m
 
-theorem eqOfBeqEqTt : ∀ {n m : Nat}, beq n m = tt → n = m
+theorem eqOfBeqEqTt : ∀ {n m : Nat}, beq n m = true → n = m
 | zero     zero     h := rfl
 | zero     (succ m) h := Bool.noConfusion h
 | (succ n) zero     h := Bool.noConfusion h
 | (succ n) (succ m) h :=
-  have beq n m = tt, from h,
+  have beq n m = true, from h,
   have n = m, from eqOfBeqEqTt this,
   congrArg succ this
 
-theorem neOfBeqEqFf : ∀ {n m : Nat}, beq n m = ff → n ≠ m
+theorem neOfBeqEqFf : ∀ {n m : Nat}, beq n m = false → n ≠ m
 | zero     zero     h₁ h₂ := Bool.noConfusion h₁
 | zero     (succ m) h₁ h₂ := Nat.noConfusion h₂
 | (succ n) zero     h₁ h₂ := Nat.noConfusion h₂
 | (succ n) (succ m) h₁ h₂ :=
-  have beq n m = ff, from h₁,
+  have beq n m = false, from h₁,
   have n ≠ m, from neOfBeqEqFf this,
   Nat.noConfusion h₂ (λ h₂, absurd h₂ this)
 
 @[extern cpp "lean::nat_dec_eq"]
 protected def decEq (n m : @& Nat) : Decidable (n = m) :=
-if h : beq n m = tt then isTrue (eqOfBeqEqTt h)
+if h : beq n m = true then isTrue (eqOfBeqEqTt h)
 else isFalse (neOfBeqEqFf (eqFfOfNeTt h))
 
 @[inline] instance : DecidableEq Nat :=
@@ -46,13 +46,13 @@ else isFalse (neOfBeqEqFf (eqFfOfNeTt h))
 
 @[extern cpp "lean::nat_dec_le"]
 def ble : Nat → Nat → Bool
-| zero     zero     := tt
-| zero     (succ m) := tt
-| (succ n) zero     := ff
+| zero     zero     := true
+| zero     (succ m) := true
+| (succ n) zero     := false
 | (succ n) (succ m) := ble n m
 
 protected def le (n m : Nat) : Prop :=
-ble n m = tt
+ble n m = true
 
 instance : HasLe Nat :=
 ⟨Nat.le⟩
@@ -261,7 +261,7 @@ predLePred
 
 @[extern cpp "lean::nat_dec_le"]
 instance decLe (n m : @& Nat) : Decidable (n ≤ m) :=
-decEq (ble n m) tt
+decEq (ble n m) true
 
 @[extern cpp "lean::nat_dec_lt"]
 instance decLt (n m : @& Nat) : Decidable (n < m) :=
diff --git a/library/init/data/nat/bitwise.lean b/library/init/data/nat/bitwise.lean
index 705243a6ab..1572786efa 100644
--- a/library/init/data/nat/bitwise.lean
+++ b/library/init/data/nat/bitwise.lean
@@ -8,8 +8,8 @@ import init.data.nat.basic init.data.nat.div init.coe
 namespace Nat
 
 def bitwise (f : Bool → Bool → Bool) : Nat → Nat → Nat | n m :=
-if n = 0 then      (if f ff tt then m else 0)
-else if m = 0 then (if f tt ff then n else 0)
+if n = 0 then      (if f false true then m else 0)
+else if m = 0 then (if f true false then n else 0)
 else
   let n' := n / 2 in
   let m' := m / 2 in
diff --git a/library/init/data/option/basic.lean b/library/init/data/option/basic.lean
index 3f2c350c50..9a8c8cd2dd 100644
--- a/library/init/data/option/basic.lean
+++ b/library/init/data/option/basic.lean
@@ -24,16 +24,16 @@ def get {α : Type u} [Inhabited α] : Option α → α
 | none     := default α
 
 def toBool {α : Type u} : Option α → Bool
-| (some _) := tt
-| none     := ff
+| (some _) := true
+| none     := false
 
 def isSome {α : Type u} : Option α → Bool
-| (some _) := tt
-| none     := ff
+| (some _) := true
+| none     := false
 
 def isNone {α : Type u} : Option α → Bool
-| (some _) := ff
-| none     := tt
+| (some _) := false
+| none     := true
 
 @[inline] protected def bind {α : Type u} {β : Type v} : Option α → (α → Option β) → Option β
 | none     b := none
diff --git a/library/init/data/rbmap/basic.lean b/library/init/data/rbmap/basic.lean
index 15a5e2bba6..41b35d8a3c 100644
--- a/library/init/data/rbmap/basic.lean
+++ b/library/init/data/rbmap/basic.lean
@@ -47,11 +47,11 @@ protected def max : Rbnode α β → Option (Σ k : α, β k)
 | (Node _ l k v r)   b := revFold l (f k v (revFold r b))
 
 @[specialize] def all (p : Π k : α, β k → Bool) : Rbnode α β → Bool
-| leaf                 := tt
+| leaf                 := true
 | (Node _ l k v r)     := p k v && all l && all r
 
 @[specialize] def any (p : Π k : α, β k → Bool) : Rbnode α β → Bool
-| leaf                 := ff
+| leaf                 := false
 | (Node _ l k v r)   := p k v || any l || any r
 
 def balance1 : Rbnode α β → Rbnode α β → Rbnode α β
@@ -67,8 +67,8 @@ def balance2 : Rbnode α β → Rbnode α β → Rbnode α β
 | _                                                        _    := leaf -- unreachable
 
 def isRed : Rbnode α β → Bool
-| (Node red _ _ _ _) := tt
-| _                  := ff
+| (Node red _ _ _ _) := true
+| _                  := false
 
 section insert
 
@@ -167,8 +167,8 @@ t.val.depth f
 t.mfold (λ k v _, f k v *> pure ⟨⟩) ⟨⟩
 
 @[inline] def Empty : Rbmap α β lt → Bool
-| ⟨leaf, _⟩ := tt
-| _         := ff
+| ⟨leaf, _⟩ := true
+| _         := false
 
 @[specialize] def toList : Rbmap α β lt → List (α × β)
 | ⟨t, _⟩ := t.revFold (λ k v ps, (k, v)::ps) []
diff --git a/library/init/data/repr.lean b/library/init/data/repr.lean
index 21be8853cf..2ef3bcccf9 100644
--- a/library/init/data/repr.lean
+++ b/library/init/data/repr.lean
@@ -19,19 +19,19 @@ instance {α : Type u} [HasRepr α] : HasRepr (id α) :=
 inferInstanceAs (HasRepr α)
 
 instance : HasRepr Bool :=
-⟨λ b, cond b "tt" "ff"⟩
+⟨λ b, cond b "true" "false"⟩
 
 instance {p : Prop} : HasRepr (Decidable p) :=
-⟨λ b : Decidable p, @ite p b _ "tt" "ff"⟩
+⟨λ b : Decidable p, @ite p b _ "true" "false"⟩
 
 protected def List.reprAux {α : Type u} [HasRepr α] : Bool → List α → String
-| b  []      := ""
-| tt (x::xs) := repr x ++ List.reprAux ff xs
-| ff (x::xs) := ", " ++ repr x ++ List.reprAux ff xs
+| b     []      := ""
+| true  (x::xs) := repr x ++ List.reprAux false xs
+| false (x::xs) := ", " ++ repr x ++ List.reprAux false xs
 
 protected def List.repr {α : Type u} [HasRepr α] : List α → String
 | []      := "[]"
-| (x::xs) := "[" ++ List.reprAux tt (x::xs) ++ "]"
+| (x::xs) := "[" ++ List.reprAux true (x::xs) ++ "]"
 
 instance {α : Type u} [HasRepr α] : HasRepr (List α) :=
 ⟨List.repr⟩
@@ -119,7 +119,7 @@ def String.quoteAux : List Char → String
 | (x::xs) := Char.quoteCore x ++ String.quoteAux xs
 
 def String.quote (s : String) : String :=
-if s.isEmpty = tt then "\"\""
+if s.isEmpty = true then "\"\""
 else "\"" ++ String.quoteAux s.toList ++ "\""
 
 instance : HasRepr String :=
diff --git a/library/init/data/string/basic.lean b/library/init/data/string/basic.lean
index 004ba4f22b..9e58762005 100644
--- a/library/init/data/string/basic.lean
+++ b/library/init/data/string/basic.lean
@@ -214,7 +214,7 @@ def forward : Iterator → Nat → Iterator
 def remainingToString : Iterator → String
 | ⟨s, _, i⟩ := s.extract i s.bsize
 
-/- (isPrefixOfRemaining it₁ it₂) is `tt` Iff `it₁.remainingToString` is a prefix
+/- (isPrefixOfRemaining it₁ it₂) is `true` Iff `it₁.remainingToString` is a prefix
    of `it₂.remainingToString`. -/
 def isPrefixOfRemaining : Iterator → Iterator → Bool
 | ⟨s₁, _, i₁⟩ ⟨s₂, _, i₂⟩ := s₁.extract i₁ s₁.bsize = s₂.extract i₂ (i₂ + (s₁.bsize - i₁))
@@ -264,7 +264,7 @@ end Iterator
 private def lineColumnAux : Nat → String.Iterator → Nat × Nat → Nat × Nat
 | 0     it r           := r
 | (k+1) it r@(line, col) :=
-  if it.hasNext = ff then r
+  if it.hasNext = false then r
   else match it.curr with
        | '\n'  := lineColumnAux k it.next (line+1, 0)
        | other := lineColumnAux k it.next (line, col+1)
diff --git a/library/init/data/tostring.lean b/library/init/data/tostring.lean
index 8311bf4554..31d296bbd2 100644
--- a/library/init/data/tostring.lean
+++ b/library/init/data/tostring.lean
@@ -25,20 +25,20 @@ instance : HasToString String.Iterator :=
 ⟨λ it, it.remainingToString⟩
 
 instance : HasToString Bool :=
-⟨λ b, cond b "tt" "ff"⟩
+⟨λ b, cond b "true" "false"⟩
 
 instance {p : Prop} : HasToString (Decidable p) :=
 -- Remark: type class inference will not consider local instance `b` in the new Elaborator
-⟨λ b : Decidable p, @ite p b _ "tt" "ff"⟩
+⟨λ b : Decidable p, @ite p b _ "true" "false"⟩
 
 protected def List.toStringAux {α : Type u} [HasToString α] : Bool → List α → String
-| b  []      := ""
-| tt (x::xs) := toString x ++ List.toStringAux ff xs
-| ff (x::xs) := ", " ++ toString x ++ List.toStringAux ff xs
+| b     []      := ""
+| true  (x::xs) := toString x ++ List.toStringAux false xs
+| false (x::xs) := ", " ++ toString x ++ List.toStringAux false xs
 
 protected def List.toString {α : Type u} [HasToString α] : List α → String
 | []      := "[]"
-| (x::xs) := "[" ++ List.toStringAux tt (x::xs) ++ "]"
+| (x::xs) := "[" ++ List.toStringAux true (x::xs) ++ "]"
 
 instance {α : Type u} [HasToString α] : HasToString (List α) :=
 ⟨List.toString⟩
diff --git a/library/init/io.lean b/library/init/io.lean
index f540946725..3b9f6ca3ca 100644
--- a/library/init/io.lean
+++ b/library/init/io.lean
@@ -76,7 +76,7 @@ constant putStr (s: @& String) : IO Unit := default _
 @[extern 1 "lean_io_prim_get_line"]
 constant getLine : IO String := default _
 @[extern 4 "lean_io_prim_handle_mk"]
-constant handle.mk (s : @& String) (m : Mode) (bin : Bool := ff) : IO handle := default _
+constant handle.mk (s : @& String) (m : Mode) (bin : Bool := false) : IO handle := default _
 @[extern 2 "lean_io_prim_handle_is_eof"]
 constant handle.isEof (h : @& handle) : IO Bool := default _
 @[extern 2 "lean_io_prim_handle_flush"]
@@ -109,7 +109,7 @@ end
 namespace Fs
 variables {m : Type → Type} [Monad m] [monadIO m]
 
-def handle.mk (s : String) (Mode : Mode) (bin : Bool := ff) : m handle := Prim.liftIO (Prim.handle.mk s Mode bin)
+def handle.mk (s : String) (Mode : Mode) (bin : Bool := false) : m handle := Prim.liftIO (Prim.handle.mk s Mode bin)
 def handle.isEof : handle → m Bool := Prim.liftIO ∘ Prim.handle.isEof
 def handle.flush : handle → m Unit := Prim.liftIO ∘ Prim.handle.flush
 def handle.close : handle → m Unit := Prim.liftIO ∘ Prim.handle.flush
@@ -143,13 +143,13 @@ Prim.liftIO $ Prim.iterate "" $ λ r, do
     c ← h.getLine,
     pure $ Sum.inl (r ++ c) -- continue
 
-def readFile (fname : String) (bin := ff) : m String :=
+def readFile (fname : String) (bin := false) : m String :=
 do h ← handle.mk fname Mode.read bin,
    r ← h.readToEnd,
    h.close,
    pure r
 
--- def writeFile (fname : String) (data : String) (bin := ff) : m Unit :=
+-- def writeFile (fname : String) (data : String) (bin := false) : m Unit :=
 -- do h ← handle.mk fname Mode.write bin,
 --   h.write data,
 --   h.close
diff --git a/library/init/lean/compiler/constfolding.lean b/library/init/lean/compiler/constfolding.lean
index 6ecb91c11d..c8157df68f 100644
--- a/library/init/lean/compiler/constfolding.lean
+++ b/library/init/lean/compiler/constfolding.lean
@@ -93,10 +93,10 @@ mkBinApp (mkBinApp (Expr.const `HasLt.le [Level.zero]) (Expr.const `Nat []) (Exp
 
 def toDecidableExpr (beforeErasure : Bool) (pred : Expr) (r : Bool) : Expr :=
 match beforeErasure, r with
-| ff, tt := mkDecIsTrue  neutralExpr neutralExpr
-| ff, ff := mkDecIsFalse neutralExpr neutralExpr
-| tt, tt := mkDecIsTrue pred (mkLcProof pred)
-| tt, ff := mkDecIsFalse pred (mkLcProof pred)
+| false, true  := mkDecIsTrue  neutralExpr neutralExpr
+| false, false := mkDecIsFalse neutralExpr neutralExpr
+| true,  true  := mkDecIsTrue pred (mkLcProof pred)
+| true,  false := mkDecIsFalse pred (mkLcProof pred)
 
 def foldNatBinPred (mkPred : Expr → Expr → Expr) (fn : Nat → Nat → Bool)
                       (beforeErasure : Bool) (a₁ a₂ : Expr) : Option Expr :=
diff --git a/library/init/lean/compiler/ir.lean b/library/init/lean/compiler/ir.lean
index e9ca6a7809..0a5d1dbbc8 100644
--- a/library/init/lean/compiler/ir.lean
+++ b/library/init/lean/compiler/ir.lean
@@ -46,16 +46,16 @@ inductive IRType
 | irrelevant | object | tobject
 
 def IRType.beq : IRType → IRType → Bool
-| IRType.float      IRType.float      := tt
-| IRType.Uint8      IRType.Uint8      := tt
-| IRType.Uint16     IRType.Uint16     := tt
-| IRType.Uint32     IRType.Uint32     := tt
-| IRType.Uint64     IRType.Uint64     := tt
-| IRType.Usize      IRType.Usize      := tt
-| IRType.irrelevant IRType.irrelevant := tt
-| IRType.object     IRType.object     := tt
-| IRType.tobject    IRType.tobject    := tt
-| _               _               := ff
+| 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.Usize      IRType.Usize      := true
+| IRType.irrelevant IRType.irrelevant := true
+| IRType.object     IRType.object     := true
+| IRType.tobject    IRType.tobject    := true
+| _               _                   := false
 
 instance IRType.HasBeq : HasBeq IRType := ⟨IRType.beq⟩
 
@@ -74,7 +74,7 @@ inductive Litval
 def Litval.beq : Litval → Litval → Bool
 | (Litval.num v₁) (Litval.num v₂) := v₁ = v₂
 | (Litval.str v₁) (Litval.str v₂) := v₁ = v₂
-| _               _               := ff
+| _               _               := false
 
 instance Litval.HasBeq : HasBeq Litval := ⟨Litval.beq⟩
 
@@ -146,9 +146,9 @@ inductive Fnbody
    `ty` must not be `object`, `tobject`, `irrelevant` nor `Usize`. -/
 | sset (x : varid) (i : Nat) (offset : Nat) (y : varid) (ty : IRType) (b : Fnbody)
 | release (x : varid) (i : Nat) (b : Fnbody)
-/- RC increment for `object`. If c = `tt`, then `inc` must check whether `x` is a tagged pointer or not. -/
+/- RC increment for `object`. If c = `true`, then `inc` must check whether `x` is a tagged pointer or not. -/
 | inc (x : varid) (n : Nat) (c : Bool) (b : Fnbody)
-/- RC decrement for `object`. If c = `tt`, then `inc` must check whether `x` is a tagged pointer or not. -/
+/- RC decrement for `object`. If c = `true`, then `inc` must check whether `x` is a tagged pointer or not. -/
 | dec (x : varid) (n : Nat) (c : Bool) (b : Fnbody)
 | mdata (d : Kvmap) (b : Fnbody)
 | case (tid : Name) (x : varid) (cs : List (AltCore Fnbody))
@@ -165,19 +165,19 @@ inductive Decl
 | fdecl  (f : fid) (xs : List Param) (ty : IRType) (b : Fnbody)
 | extern (f : fid) (xs : List Param) (ty : IRType)
 
-/-- `Expr.isPure e` return `tt` Iff `e` is in the `λPure` fragment. -/
+/-- `Expr.isPure e` return `true` Iff `e` is in the `λPure` fragment. -/
 def Expr.isPure : Expr → Bool
-| (Expr.ctor _ _)  := tt
-| (Expr.proj _ _)  := tt
-| (Expr.uproj _ _) := tt
-| (Expr.sproj _ _) := tt
-| (Expr.fap _ _)   := tt
-| (Expr.pap _ _)   := tt
-| (Expr.ap _ _)    := tt
-| (Expr.lit _)     := tt
-| _                := ff
+| (Expr.ctor _ _)  := true
+| (Expr.proj _ _)  := true
+| (Expr.uproj _ _) := true
+| (Expr.sproj _ _) := true
+| (Expr.fap _ _)   := true
+| (Expr.pap _ _)   := true
+| (Expr.ap _ _)    := true
+| (Expr.lit _)     := true
+| _                := false
 
-/-- `Fnbody.isPure b` return `tt` Iff `b` is in the `λPure` fragment. -/
+/-- `Fnbody.isPure b` return `true` Iff `b` is in the `λPure` fragment. -/
 mutual def Fnbody.isPure, alts.isPure, alt.isPure
 with Fnbody.isPure : Fnbody → Bool
 | (Fnbody.vdecl _ _ e b)    := e.isPure && b.isPure
@@ -186,16 +186,16 @@ with Fnbody.isPure : Fnbody → Bool
 | (Fnbody.sset _ _ _ _ _ b) := b.isPure
 | (Fnbody.mdata _ b)        := b.isPure
 | (Fnbody.case _ _ cs)      := alts.isPure cs
-| (Fnbody.ret _)            := tt
-| (Fnbody.jmp _ _)          := tt
-| Fnbody.unreachable        := tt
-| _                         := ff
+| (Fnbody.ret _)            := true
+| (Fnbody.jmp _ _)          := true
+| Fnbody.unreachable        := true
+| _                         := false
 with alts.isPure : List alt → Bool
-| []      := tt
+| []      := true
 | (a::as) := a.isPure && alts.isPure as
 with alt.isPure : alt → Bool
 | (alt.ctor _ b)  := b.isPure
-| (alt.default b) := ff
+| (alt.default b) := false
 
 abbrev varRenaming := NameMap Name
 
@@ -213,15 +213,15 @@ instance varid.hasAeqv : HasAlphaEqv varid := ⟨varid.alphaEqv⟩
 
 def Arg.alphaEqv (ρ : varRenaming) : Arg → Arg → Bool
 | (Arg.var v₁)   (Arg.var v₂)   := v₁ =[ρ]= v₂
-| Arg.irrelevant Arg.irrelevant := tt
-| _              _              := ff
+| Arg.irrelevant Arg.irrelevant := true
+| _              _              := false
 
 instance Arg.hasAeqv : HasAlphaEqv Arg := ⟨Arg.alphaEqv⟩
 
 def args.alphaEqv (ρ : varRenaming) : List Arg → List Arg → Bool
-| []      []      := tt
+| []      []      := true
 | (a::as) (b::bs) := a =[ρ]= b && args.alphaEqv as bs
-| _       _       := ff
+| _       _       := false
 
 instance args.hasAeqv : HasAlphaEqv (List Arg) := ⟨args.alphaEqv⟩
 
@@ -240,7 +240,7 @@ def Expr.alphaEqv (ρ : varRenaming) : Expr → Expr → Bool
 | (Expr.lit v₁)           (Expr.lit v₂)           := v₁ == v₂
 | (Expr.isShared x₁)     (Expr.isShared x₂)     := x₁ =[ρ]= x₂
 | (Expr.isTaggedPtr x₁) (Expr.isTaggedPtr x₂) := x₁ =[ρ]= x₂
-| _                        _                      := ff
+| _                        _                      := false
 
 instance Expr.hasAeqv : HasAlphaEqv Expr:= ⟨Expr.alphaEqv⟩
 
@@ -262,7 +262,7 @@ with Fnbody.alphaEqv : varRenaming → Fnbody → Fnbody → Bool
 | ρ (Fnbody.jdecl j₁ ys₁ t₁ v₁ b₁)  (Fnbody.jdecl j₂ ys₂ t₂ v₂ b₂)    :=
   (match addParamsRename ρ ys₁ ys₂ with
    | some ρ' := t₁ == t₂ && Fnbody.alphaEqv ρ' v₁ v₂ && Fnbody.alphaEqv (addVarRename ρ j₁ j₂) b₁ b₂
-   | none    := ff)
+   | none    := false)
 | ρ (Fnbody.set x₁ i₁ y₁ b₁)        (Fnbody.set x₂ i₂ y₂ b₂)          := x₁ =[ρ]= x₂ && i₁ = i₂ && y₁ =[ρ]= y₂ && Fnbody.alphaEqv ρ b₁ b₂
 | ρ (Fnbody.uset x₁ i₁ y₁ b₁)       (Fnbody.uset x₂ i₂ y₂ b₂)         := x₁ =[ρ]= x₂ && i₁ = i₂ && y₁ =[ρ]= y₂ && Fnbody.alphaEqv ρ b₁ b₂
 | ρ (Fnbody.sset x₁ i₁ o₁ y₁ t₁ b₁) (Fnbody.sset x₂ i₂ o₂ y₂ t₂ b₂)   :=
@@ -274,16 +274,16 @@ with Fnbody.alphaEqv : varRenaming → Fnbody → Fnbody → Bool
 | ρ (Fnbody.case n₁ x₁ as₁)         (Fnbody.case n₂ x₂ as₂)           := n₁ = n₂ && x₁ =[ρ]= x₂ && alts.alphaEqv ρ as₁ as₂
 | ρ (Fnbody.jmp j₁ ys₁)             (Fnbody.jmp j₂ ys₂)               := j₁ = j₂ && ys₁ =[ρ]= ys₂
 | ρ (Fnbody.ret x₁)                 (Fnbody.ret x₂)                   := x₁ =[ρ]= x₂
-| _ Fnbody.unreachable              Fnbody.unreachable                := tt
-| _ _                               _                                 := ff
+| _ Fnbody.unreachable              Fnbody.unreachable                := true
+| _ _                               _                                 := false
 with alts.alphaEqv : varRenaming → List alt → List alt → Bool
-| _ []        []        := tt
+| _ []        []        := true
 | ρ (a₁::as₁) (a₂::as₂) := alt.alphaEqv ρ a₁ a₂ && alts.alphaEqv ρ as₁ as₂
-| _ _         _         := ff
+| _ _         _         := false
 with alt.alphaEqv : varRenaming → alt → alt → Bool
 | ρ (alt.ctor i₁ b₁) (alt.ctor i₂ b₂) := i₁ == i₂ && Fnbody.alphaEqv ρ b₁ b₂
 | ρ (alt.default b₁) (alt.default b₂) := Fnbody.alphaEqv ρ b₁ b₂
-| _ _                _                := ff
+| _ _                _                := false
 
 def Fnbody.beq (b₁ b₂ : Fnbody) : Bool :=
 Fnbody.alphaEqv mkNameMap b₁ b₂
diff --git a/library/init/lean/declaration.lean b/library/init/lean/declaration.lean
index 8a55af5960..d394278366 100644
--- a/library/init/lean/declaration.lean
+++ b/library/init/lean/declaration.lean
@@ -84,7 +84,7 @@ structure inductiveVal extends ConstantVal :=
 (nindices : Nat)      -- Number of indices
 (all : List Name)     -- List of all (including this one) inductive datatypes in the mutual Declaration containing this one
 (cnstrs : List Name)  -- List of all constructors for this inductive datatype
-(isRec : Bool)       -- `tt` Iff it is recursive
+(isRec : Bool)       -- `true` Iff it is recursive
 (isUnsafe : Bool)
 (isReflexive : Bool)
 
diff --git a/library/init/lean/elaborator.lean b/library/init/lean/elaborator.lean
index 8023ad0abe..763bd75660 100644
--- a/library/init/lean/elaborator.lean
+++ b/library/init/lean/elaborator.lean
@@ -16,7 +16,7 @@ namespace Lean
 constant environment : Type := Unit
 
 @[extern "lean_environment_contains"]
-constant environment.contains (env : @& environment) (n : @& Name) : Bool := ff
+constant environment.contains (env : @& environment) (n : @& Name) : Bool := false
 -- deprecated Constructor
 @[extern "lean_expr_local"]
 constant Expr.local (n : Name) (pp : Name) (ty : Expr) (bi : BinderInfo) : Expr := default Expr
@@ -287,14 +287,14 @@ def toPexpr : Syntax → ElaboratorM Expr
     let v := view structInst stx,
     -- order should be: fields*, sources*, catchall?
     let (fields, other) := v.items.span (λ it, ↑match SepBy.Elem.View.item it with
-      | structInstItem.View.field _ := tt
-      | _ := ff),
+      | structInstItem.View.field _ := true
+      | _ := false),
     let (sources, catchall) := other.span (λ it, ↑match SepBy.Elem.View.item it with
-      | structInstItem.View.source {source := some _} := tt
-      | _ := ff),
+      | structInstItem.View.source {source := some _} := true
+      | _ := false),
     catchall ← match catchall with
-    | [] := pure ff
-    | [{item := structInstItem.View.source _}] := pure tt
+    | [] := pure false
+    | [{item := structInstItem.View.source _}] := pure true
     | {item := it}::_ := error (review structInstItem it) $ "unexpected item in structure instance notation",
 
     fields ← fields.mmap (λ f, match SepBy.Elem.View.item f with
@@ -325,7 +325,7 @@ def toPexpr : Syntax → ElaboratorM Expr
     let eqns := mkEqns type eqns,
     Expr.mdata mdata e ← pure eqns
       | error stx "toPexpr: unreachable",
-    let eqns := Expr.mdata (mdata.setBool `match tt) e,
+    let eqns := Expr.mdata (mdata.setBool `match true) e,
     Expr.mkApp eqns <$> v.scrutinees.mmap (λ scr, toPexpr scr.item)
   | _ := error stx $ "toPexpr: unexpected Node: " ++ toString k.name,
   (match k with
@@ -386,8 +386,8 @@ def declModifiersToPexpr (mods : declModifiers.View) : ElaboratorM Expr := do
     | some {doc := some doc, ..} := mdata.setString `docString doc.val
     | _ := mdata,
   let mdata := match mods.visibility with
-    | some (visibility.View.private _) := mdata.setBool `private tt
-    | some (visibility.View.protected _) := mdata.setBool `protected tt
+    | some (visibility.View.private _) := mdata.setBool `private true
+    | some (visibility.View.protected _) := mdata.setBool `protected true
     | _ := mdata,
   let mdata := mdata.setBool `noncomputable mods.noncomputable.isSome,
   let mdata := mdata.setBool `unsafe mods.unsafe.isSome,
@@ -587,8 +587,8 @@ def variables.elaborate : Elaborator :=
         modifyCurrentScope $ λ sc, {sc with vars :=
           sc.vars.insert id {v with BinderInfo := bi}}
       | none := error (Syntax.ident id) "",
-      pure ff
-    else pure tt
+      pure false
+    else pure true
   | _ := error stx "variables.elaborate: unexpected input",
   vars ← simpleBindersToPexpr vars,
   oldElabCommand stx $ Expr.mdata mdata vars
@@ -705,9 +705,9 @@ def reserveNotation.elaborate : Elaborator :=
   updateParserConfig
 
 def matchPrecedence : Option precedence.View → Option precedence.View → Bool
-| none      (some rp) := tt
+| none      (some rp) := true
 | (some sp) (some rp) := sp.Term.toNat = rp.Term.toNat
-| _         _         := ff
+| _         _         := false
 
 /-- Check if a notation is compatible with a reserved notation, and if so, copy missing
     precedences in the notation from the reserved notation. -/
@@ -774,8 +774,8 @@ def notation.elaborate : Elaborator :=
   let nota := view «notation» stx,
   -- HACK: ignore List Literal notation using :fold
   let usesFold := nota.spec.rules.any $ λ r, match r.transition with
-    | some (transition.View.Arg {action := some {kind := actionKind.View.fold _, ..}, ..}) := tt
-    | _ := ff,
+    | some (transition.View.Arg {action := some {kind := actionKind.View.fold _, ..}, ..}) := true
+    | _ := false,
   if usesFold then do {
     cfg ← read,
     modify $ λ st, {st with messages := st.messages.add {filename := cfg.filename, pos := ⟨1,0⟩,
@@ -842,7 +842,7 @@ def setOption.elaborate : Elaborator :=
   let opts := sc.Options,
   -- TODO(Sebastian): check registered Options
   let opts := match v.val with
-  | optionValue.View.Bool b := opts.setBool opt (match b with boolOptionValue.View.True _ := tt | _ := ff)
+  | optionValue.View.Bool b := opts.setBool opt (match b with boolOptionValue.View.True _ := true | _ := false)
   | optionValue.View.String lit := (match lit.value with
     | some s := opts.setString opt s
     | none   := opts)  -- Parser already failed
@@ -917,19 +917,19 @@ def elaborators : Rbmap Name Elaborator (<) := Rbmap.fromList [
 
 -- TODO: optimize
 def isOpenNamespace (sc : Scope) : Name → Bool
-| Name.anonymous := tt
+| Name.anonymous := true
 | ns :=
   -- check surrounding namespaces
   ns ∈ sc.nsStack ∨
   -- check opened namespaces
   sc.openDecls.any (λ od, od.id.val = ns) ∨
   -- TODO: check active exports
-  ff
+  false
 
 -- TODO: `hiding`, `as`, `renaming`
 def matchOpenSpec (n : Name) (spec : openSpec.View) : Option Name :=
 let matchesOnly := match spec.only with
-| none := tt
+| none := true
 | some only := n = only.id.val ∨ only.ids.any (λ id, n = id.val) in
 if matchesOnly then some (spec.id.val ++ n) else none
 
@@ -954,7 +954,7 @@ def resolveContext : Name → ElaboratorM (List Name)
   -- check environment directly
   (let unrooted := n.replacePrefix `_root_ Name.anonymous in
    match st.env.contains unrooted with
-   | tt := [unrooted]
+   | true := [unrooted]
    | _ := [])
   ++
   -- check opened namespaces
diff --git a/library/init/lean/expander.lean b/library/init/lean/expander.lean
index 73b1ce3080..a72a6aa8ea 100644
--- a/library/init/lean/expander.lean
+++ b/library/init/lean/expander.lean
@@ -466,7 +466,7 @@ def universes.transform : transformer :=
   pure $ Syntax.list $ v.ids.map (λ id, review «universe» {id := id})
 
 def sorry.transform : transformer :=
-λ stx, pure $ mkApp (globId `sorryAx) [review hole {}, globId `Bool.ff]
+λ stx, pure $ mkApp (globId `sorryAx) [review hole {}, globId `Bool.false]
 
 local attribute [instance] Name.hasLtQuick
 
diff --git a/library/init/lean/format.lean b/library/init/lean/format.lean
index ae55745649..db3a65c402 100644
--- a/library/init/lean/format.lean
+++ b/library/init/lean/format.lean
@@ -18,30 +18,30 @@ inductive Format
 | choice       : Format → Format → Format
 
 namespace Format
-instance : HasAppend Format     := ⟨compose ff⟩
+instance : HasAppend Format     := ⟨compose false⟩
 instance : HasCoe String Format := ⟨text⟩
 
 def join (xs : List Format) : Format :=
 xs.foldl (++) ""
 
 def flatten : Format → Format
-| nil                  := nil
-| line                 := text " "
-| f@(text _)           := f
-| (nest _ f)           := flatten f
-| (choice f _)         := flatten f
-| f@(compose tt _ _)   := f
-| f@(compose ff f₁ f₂) := compose tt (flatten f₁) (flatten f₂)
+| nil                     := nil
+| line                    := text " "
+| f@(text _)              := f
+| (nest _ f)              := flatten f
+| (choice f _)            := flatten f
+| f@(compose true _ _)    := f
+| f@(compose false f₁ f₂) := compose true (flatten f₁) (flatten f₂)
 
 def group : Format → Format
-| nil                := nil
-| f@(text _)         := f
-| f@(compose tt _ _) := f
-| f                  := choice (flatten f) f
+| nil                  := nil
+| f@(text _)           := f
+| f@(compose true _ _) := f
+| f                    := choice (flatten f) f
 
 structure SpaceResult :=
-(found    := ff)
-(exceeded := ff)
+(found    := false)
+(exceeded := false)
 (space    := 0)
 
 /-
@@ -56,7 +56,7 @@ else let y := r₂.get in
 
 def spaceUptoLine : Format → Nat → SpaceResult
 | nil               w := {}
-| line              w := { found := tt }
+| line              w := { found := true }
 | (text s)          w := { space := s.length, exceeded := s.length > w }
 | (compose _ f₁ f₂) w := merge w (spaceUptoLine f₁ w) (spaceUptoLine f₂ w)
 | (nest _ f)        w := spaceUptoLine f w
diff --git a/library/init/lean/frontend.lean b/library/init/lean/frontend.lean
index 5f21cea625..2ef77b705d 100644
--- a/library/init/lean/frontend.lean
+++ b/library/init/lean/frontend.lean
@@ -35,7 +35,7 @@ def runFrontend (filename input : String) (printMsg : Message → IO Unit) (coll
   msgs.toList.mfor printMsg,
   let expanderCfg : ExpanderConfig := {transformers := builtinTransformers, ..parserCfg},
   let elabCfg : ElaboratorConfig := {filename := filename, input := input, initialParserCfg := parserCfg, ..parserCfg},
-  let opts := Options.mk.setBool `Trace.asMessages tt,
+  let opts := Options.mk.setBool `Trace.asMessages true,
   let elabSt := Elaborator.mkState elabCfg env opts,
   let addOutput (out : Syntax) outs := if collectOutputs then out::outs else [],
   IO.Prim.iterate (pSnap, elabSt, parserCfg, expanderCfg, ([] : List Syntax)) $ λ ⟨pSnap, elabSt, parserCfg, expanderCfg, outs⟩, do {
@@ -84,7 +84,7 @@ def processFile (f s : String) (json : Bool) : StateT environment IO Unit := do
     else IO.println msg.toString,
    -- print and erase uncaught exceptions
    catch
-     (runFrontend f s printMsg ff *> pure ())
+     (runFrontend f s printMsg false *> pure ())
      (λ e, do
         monadLift (printMsg {filename := f, severity := MessageSeverity.error, pos := ⟨1, 0⟩, text := e}),
         throw e)
diff --git a/library/init/lean/kvmap.lean b/library/init/lean/kvmap.lean
index a01e143dbf..c128ff5489 100644
--- a/library/init/lean/kvmap.lean
+++ b/library/init/lean/kvmap.lean
@@ -18,7 +18,7 @@ def DataValue.beq : DataValue → DataValue → Bool
 | (DataValue.ofString s₁) (DataValue.ofString s₂) := s₁ = s₂
 | (DataValue.ofNat n₁)    (DataValue.ofNat n₂)    := n₂ = n₂
 | (DataValue.ofBool b₁)   (DataValue.ofBool b₂)   := b₁ = b₂
-| _                         _                         := ff
+| _                         _                     := false
 
 instance DataValue.HasBeq : HasBeq DataValue := ⟨DataValue.beq⟩
 
@@ -79,11 +79,11 @@ def setName (m : Kvmap) (k : Name) (v : Name) : Kvmap :=
 m.insert k (DataValue.ofName v)
 
 def subset : Kvmap → Kvmap → Bool
-| ⟨[]⟩          m₂ := tt
+| ⟨[]⟩          m₂ := true
 | ⟨(k, v₁)::m₁⟩ m₂ :=
   (match m₂.find k with
    | some v₂ := v₁ == v₂ && subset ⟨m₁⟩ m₂
-   | none    := ff)
+   | none    := false)
 
 def eqv (m₁ m₂ : Kvmap) : Bool :=
 subset m₁ m₂ && subset m₂ m₁
diff --git a/library/init/lean/level.lean b/library/init/lean/level.lean
index 61cd478ba2..2317bed139 100644
--- a/library/init/lean/level.lean
+++ b/library/init/lean/level.lean
@@ -28,18 +28,18 @@ instance levelIsInhabited : Inhabited Level :=
 def Level.one : Level := Level.succ Level.zero
 
 def Level.hasParam : Level → Bool
-| (Level.Param _)    := tt
+| (Level.Param _)    := true
 | (Level.succ l)     := Level.hasParam l
 | (Level.max l₁ l₂)  := Level.hasParam l₁ || Level.hasParam l₂
 | (Level.imax l₁ l₂) := Level.hasParam l₁ || Level.hasParam l₂
-| _                  := ff
+| _                  := false
 
 def Level.hasMvar : Level → Bool
-| (Level.mvar _)     := tt
+| (Level.mvar _)     := true
 | (Level.succ l)     := Level.hasParam l
 | (Level.max l₁ l₂)  := Level.hasParam l₁ || Level.hasParam l₂
 | (Level.imax l₁ l₂) := Level.hasParam l₁ || Level.hasParam l₂
-| _                  := ff
+| _                  := false
 
 def Level.ofNat : Nat → Level
 | 0     := Level.zero
@@ -97,8 +97,8 @@ def Result.imax : Result → Result → Result
 | f₁ f₂                   := Result.imaxNode [f₁, f₂]
 
 def parenIfFalse : Format → Bool → Format
-| f tt := f
-| f ff := f.paren
+| f true  := f
+| f false := f.paren
 
 mutual def Result.toFormat, resultList.toFormat
 with Result.toFormat : Result → Bool → Format
@@ -106,13 +106,13 @@ with Result.toFormat : Result → Bool → Format
 | (Result.num k)          _ := toString k
 | (Result.offset f 0)     r := Result.toFormat f r
 | (Result.offset f (k+1)) r :=
-  let f' := Result.toFormat f ff in
+  let f' := Result.toFormat f false in
   parenIfFalse (f' ++ "+" ++ toFmt (k+1)) r
 | (Result.maxNode Fs)    r := parenIfFalse (Format.group $ "max" ++ resultList.toFormat Fs) r
 | (Result.imaxNode Fs)   r := parenIfFalse (Format.group $ "imax" ++ resultList.toFormat Fs) r
 with resultList.toFormat : List Result → Format
 | []      := Format.nil
-| (r::rs) := Format.line ++ Result.toFormat r ff ++ resultList.toFormat rs
+| (r::rs) := Format.line ++ Result.toFormat r false ++ resultList.toFormat rs
 
 def Level.toResult : Level → Result
 | Level.zero         := Result.num 0
@@ -123,7 +123,7 @@ def Level.toResult : Level → Result
 | (Level.mvar n)     := Result.leaf (toFmt n)
 
 def Level.toFormat (l : Level) : Format :=
-(Level.toResult l).toFormat tt
+(Level.toResult l).toFormat true
 
 instance levelHasToFormat : HasToFormat Level := ⟨Level.toFormat⟩
 instance levelHasToString : HasToString Level := ⟨Format.pretty ∘ Level.toFormat⟩
diff --git a/library/init/lean/message.lean b/library/init/lean/message.lean
index c9766ea118..dd5e9e1521 100644
--- a/library/init/lean/message.lean
+++ b/library/init/lean/message.lean
@@ -54,8 +54,8 @@ instance : HasAppend MessageLog :=
 
 def hasErrors (log : MessageLog) : Bool :=
 log.revList.any $ λ m, match m.severity with
-| MessageSeverity.error := tt
-| _                      := ff
+| MessageSeverity.error := true
+| _                     := false
 
 def toList (log : MessageLog) : List Message :=
 log.revList.reverse
diff --git a/library/init/lean/name.lean b/library/init/lean/name.lean
index 198638b414..739dd25b5d 100644
--- a/library/init/lean/name.lean
+++ b/library/init/lean/name.lean
@@ -106,24 +106,24 @@ def replacePrefix : Name → Name → Name → Name
     mkNumeral (p.replacePrefix queryP newP) s
 
 def quickLtCore : Name → Name → Bool
-| anonymous        anonymous          := ff
-| anonymous        _                  := tt
-| (mkNumeral n v) (mkNumeral n' v') := v < v' || (v = v' && n.quickLtCore n')
-| (mkNumeral _ _) (mkString _ _)    := tt
-| (mkString n s)  (mkString n' s')  := s < s' || (s = s' && n.quickLtCore n')
-| _                _                  := ff
+| anonymous        anonymous          := false
+| anonymous        _                  := true
+| (mkNumeral n v) (mkNumeral n' v')   := v < v' || (v = v' && n.quickLtCore n')
+| (mkNumeral _ _) (mkString _ _)      := true
+| (mkString n s)  (mkString n' s')    := s < s' || (s = s' && n.quickLtCore n')
+| _                _                  := false
 
 def quickLt (n₁ n₂ : Name) : Bool :=
-if n₁.hash < n₂.hash then tt
-else if n₁.hash > n₂.hash then ff
+if n₁.hash < n₂.hash then true
+else if n₁.hash > n₂.hash then false
 else quickLtCore n₁ n₂
 
 /- Alternative HasLt instance. -/
 @[inline] protected def hasLtQuick : HasLt Name :=
-⟨λ a b, Name.quickLt a b = tt⟩
+⟨λ a b, Name.quickLt a b = true⟩
 
 @[inline] instance : decidableRel (@HasLt.lt Name Name.hasLtQuick) :=
-inferInstanceAs (decidableRel (λ a b, Name.quickLt a b = tt))
+inferInstanceAs (decidableRel (λ a b, Name.quickLt a b = true))
 
 def toStringWithSep (sep : String) : Name → String
 | anonymous                := "[anonymous]"
diff --git a/library/init/lean/parser/combinators.lean b/library/init/lean/parser/combinators.lean
index 6d85222799..a94a79b6e6 100644
--- a/library/init/lean/parser/combinators.lean
+++ b/library/init/lean/parser/combinators.lean
@@ -86,11 +86,11 @@ private def sepByAux (p : m Syntax) (sep : Parser) (allowTrailingSep : Bool) : B
     | pure (Syntax.list (a::as).reverse),
   sepByAux allowTrailingSep (s::a::as) n
 
-def sepBy (p sep : Parser) (allowTrailingSep := tt) : Parser :=
-do rem ← remaining, sepByAux p sep allowTrailingSep tt [] (rem+1)
+def sepBy (p sep : Parser) (allowTrailingSep := true) : Parser :=
+do rem ← remaining, sepByAux p sep allowTrailingSep true [] (rem+1)
 
-def sepBy1 (p sep : Parser) (allowTrailingSep := tt) : Parser :=
-do rem ← remaining, sepByAux p sep allowTrailingSep ff [] (rem+1)
+def sepBy1 (p sep : Parser) (allowTrailingSep := true) : Parser :=
+do rem ← remaining, sepByAux p sep allowTrailingSep false [] (rem+1)
 
 instance sepBy.tokens (p sep : Parser) (a) [Parser.HasTokens p] [Parser.HasTokens sep] :
   Parser.HasTokens (sepBy p sep a) :=
diff --git a/library/init/lean/parser/module.lean b/library/init/lean/parser/module.lean
index e8ffe08504..81cdc8ac76 100644
--- a/library/init/lean/parser/module.lean
+++ b/library/init/lean/parser/module.lean
@@ -76,11 +76,11 @@ private def commandWrecAux : Bool → Nat → ModuleParserM (Bool × Syntax)
 | recovering 0            := error "unreachable"
 | recovering (Nat.succ n) := do
   -- terminate at EOF
-  Nat.succ _ ← remaining | (Prod.mk ff) <$> eoi.Parser,
+  Nat.succ _ ← remaining | (Prod.mk false) <$> eoi.Parser,
   (recovering, c) ← catch (do {
     cfg ← read,
     c ← monadLift $ command.Parser.run cfg.commandParsers,
-    pure (ff, some c)
+    pure (false, some c)
   } <|> do {
     -- unknown command: try to skip token, or else single character
     when (¬ recovering) $ do {
@@ -88,11 +88,11 @@ private def commandWrecAux : Bool → Nat → ModuleParserM (Bool × Syntax)
       logMessage {expected := Dlist.singleton "command", it := it, custom := some ()}
     },
     try (monadLift token *> pure ()) <|> (any *> pure ()),
-    pure (tt, none)
+    pure (true, none)
   }) $ λ msg, do {
     -- error inside command: log error, return partial Syntax tree
     logMessage msg,
-    pure (tt, some msg.custom.get)
+    pure (true, some msg.custom.get)
   },
   /- NOTE: We need to make very sure that these recursive calls are happening in tail positions.
      Otherwise, resuming the coroutine is linear in the number of previous commands. -/
@@ -120,7 +120,7 @@ match r with
 | Except.error msg  := (msg.custom.get, Except.error $ messageOfParsecMessage cfg msg)
 
 def parseHeader (cfg : ModuleParserConfig) :=
-let snap := {ModuleParserSnapshot . recovering := ff, it := cfg.input.mkIterator} in
+let snap := {ModuleParserSnapshot . recovering := false, it := cfg.input.mkIterator} in
 resumeModuleParser cfg snap (λ stx, (stx, snap)) $ do
   -- `token` assumes that there is no leading whitespace
   monadLift whitespace,
diff --git a/library/init/lean/parser/notation.lean b/library/init/lean/parser/notation.lean
index e1fe8af62b..2198cb63c8 100644
--- a/library/init/lean/parser/notation.lean
+++ b/library/init/lean/parser/notation.lean
@@ -68,7 +68,7 @@ def symbolQuote.Parser : termParser :=
 node! symbolQuote [
   leftQuote: rawStr "`",
   symbol: quotedSymbol.Parser,
-  rightQuote: rawStr "`" tt, -- consume trailing ws
+  rightQuote: rawStr "`" true, -- consume trailing ws
   prec: precedence.Parser?]
 
 def unquotedSymbol.Parser : termParser :=
diff --git a/library/init/lean/parser/parsec.lean b/library/init/lean/parser/parsec.lean
index 8ee61e4567..54127b9352 100644
--- a/library/init/lean/parser/parsec.lean
+++ b/library/init/lean/parser/parsec.lean
@@ -94,7 +94,7 @@ def eps : ParsecT μ m Unit :=
 ParsecT.pure ()
 
 protected def failure : ParsecT μ m α :=
-λ it, pure (error { unexpected := "failure", it := it, custom := none } ff)
+λ it, pure (error { unexpected := "failure", it := it, custom := none } false)
 
 def merge (msg₁ msg₂ : Message μ) : Message μ :=
 { expected := msg₁.expected ++ msg₂.expected, ..msg₁ }
@@ -102,9 +102,9 @@ def merge (msg₁ msg₂ : Message μ) : Message μ :=
 @[inlineIfReduce] def bindMkRes (ex₁ : Option (Dlist String)) (r : Result μ β) : Result μ β :=
 match ex₁, r with
 | none,     ok b it _          := ok b it none
-| none,     error msg _        := error msg tt
+| none,     error msg _        := error msg true
 | some ex₁, ok b it (some ex₂) := ok b it (some $ ex₁ ++ ex₂)
-| some ex₁, error msg₂ ff      := error { expected := ex₁ ++ msg₂.expected, .. msg₂ } ff
+| some ex₁, error msg₂ false      := error { expected := ex₁ ++ msg₂.expected, .. msg₂ } false
 | some ex₁, other              := other
 
 /--
@@ -137,10 +137,10 @@ def Monad' : Monad (ParsecT μ m) :=
 { bind := λ _ _, ParsecT.bind', pure := λ _, ParsecT.pure }
 
 instance : MonadFail Parsec' :=
-{ fail := λ _ s it, error { unexpected := s, it := it, custom := () } ff }
+{ fail := λ _ s it, error { unexpected := s, it := it, custom := () } false }
 
 instance : MonadExcept (Message μ) (ParsecT μ m) :=
-{ throw := λ _ msg it, pure (error msg ff),
+{ throw := λ _ msg it, pure (error msg false),
   catch := λ _ p c it, do
     r ← p it,
     match r with
@@ -160,7 +160,7 @@ def expect (msg : Message μ) (exp : String) : Message μ :=
 @[inlineIfReduce] def labelsMkRes (r : Result μ α) (lbls : Dlist String) : Result μ α :=
 match r with
   | ok a it (some _) := ok a it (some lbls)
-  | error msg ff     := error {expected := lbls, ..msg} ff
+  | error msg false     := error {expected := lbls, ..msg} false
   | other            := other
 
 @[inline] def labels (p : ParsecT μ m α) (lbls : Dlist String) : ParsecT μ m α :=
@@ -170,7 +170,7 @@ match r with
 
 @[inlineIfReduce] def tryMkRes (r : Result μ α) : Result μ α :=
 match r with
-| error msg _  := error msg ff
+| error msg _  := error msg false
 | other        := other
 
 /--
@@ -198,7 +198,7 @@ Without the `try` Combinator we will not be able to backtrack on the `let` keywo
 @[inlineIfReduce] def orelseMkRes (msg₁ : Message μ) (r : Result μ α) : Result μ α :=
 match r with
 | ok a it' (some ex₂) := ok a it' (some $ msg₁.expected ++ ex₂)
-| error msg₂ ff       := error (merge msg₁ msg₂) ff
+| error msg₂ false       := error (merge msg₁ msg₂) false
 | other               := other
 
 /--
@@ -217,7 +217,7 @@ match r with
 λ it, do
   r ← p it,
   match r with
-  | error msg₁ ff := do { r ← q it, pure $ orelseMkRes msg₁ r }
+  | error msg₁ false := do { r ← q it, pure $ orelseMkRes msg₁ r }
   | other         := pure other
 
 instance : Alternative (ParsecT μ m) :=
@@ -261,7 +261,7 @@ variables {m : Type → Type} [Monad m] [MonadParsec μ m] {α β : Type}
 
 def error {α : Type} (unexpected : String) (expected : Dlist String := Dlist.Empty)
           (it : Option Iterator := none) (custom : Option μ := none) : m α :=
-lift $ λ it', Result.error { unexpected := unexpected, expected := expected, it := it.getOrElse it', custom := custom } ff
+lift $ λ it', Result.error { unexpected := unexpected, expected := expected, it := it.getOrElse it', custom := custom } false
 
 @[inline] def leftOver : m Iterator :=
 lift $ λ it, Result.mkEps it it
@@ -315,7 +315,7 @@ do it ← leftOver,
        else pure ()
 
 def eoiError (it : Iterator) : Result μ α :=
-Result.error { it := it, unexpected := "end of input", custom := default _ } ff
+Result.error { it := it, unexpected := "end of input", custom := default _ } false
 
 def curr : m Char :=
 String.Iterator.curr <$> leftOver
@@ -368,7 +368,7 @@ def strCore (s : String) (ex : Dlist String) : m String :=
 if s.isEmpty then pure ""
 else lift $ λ it, match strAux s.length s.mkIterator it with
   | some it' := Result.ok s it' none
-  | none     := Result.error { it := it, expected := ex, custom := none } ff
+  | none     := Result.error { it := it, expected := ex, custom := none } false
 
 @[inline] def str (s : String) : m String :=
 strCore s (Dlist.singleton (repr s))
@@ -398,9 +398,9 @@ private def takeWhileAux (p : Char → Bool) : Nat → String → Iterator → R
        else mkStringResult r it
 
 /--
-Consume input as long as the predicate returns `tt`, and return the consumed input.
+Consume input as long as the predicate returns `true`, and return the consumed input.
 This Parser does not fail. It will return an Empty String if the predicate
-returns `ff` on the current character. -/
+returns `false` on the current character. -/
 @[specialize] def takeWhile (p : Char → Bool) : m String :=
 lift $ λ it, takeWhileAux p it.remaining "" it
 
@@ -408,14 +408,14 @@ lift $ λ it, takeWhileAux p it.remaining "" it
 lift $ λ it, takeWhileAux p it.remaining ini it
 
 /--
-Consume input as long as the predicate returns `tt`, and return the consumed input.
+Consume input as long as the predicate returns `true`, and return the consumed input.
 This Parser requires the predicate to succeed on at least once. -/
 @[specialize] def takeWhile1 (p : Char → Bool) : m String :=
 do c ← satisfy p,
    takeWhileCont p (toString c)
 
 /--
-Consume input as long as the predicate returns `ff` (i.e. until it returns `tt`), and return the consumed input.
+Consume input as long as the predicate returns `false` (i.e. until it returns `true`), and return the consumed input.
 This Parser does not fail. -/
 @[inline] def takeUntil (p : Char → Bool) : m String :=
 takeWhile (λ c, !p c)
@@ -432,12 +432,12 @@ else Result.mkEps () it
 | (n+1) consumed it :=
   if !it.hasNext then mkConsumedResult consumed it
   else let c := it.curr in
-       if p c then takeWhileAux' n tt it.next
+       if p c then takeWhileAux' n true it.next
        else mkConsumedResult consumed it
 
 /-- Similar to `takeWhile` but it does not return the consumed input. -/
 @[specialize] def takeWhile' (p : Char → Bool) : m Unit :=
-lift $ λ it, takeWhileAux' p it.remaining ff it
+lift $ λ it, takeWhileAux' p it.remaining false it
 
 /-- Similar to `takeWhile1` but it does not return the consumed input. -/
 @[specialize] def takeWhile1' (p : Char → Bool) : m Unit :=
@@ -469,7 +469,7 @@ String.Iterator.offset <$> leftOver
 /-- `notFollowedBy p` succeeds when Parser `p` fails -/
 @[inline] def notFollowedBy [MonadExcept (Message μ) m] (p : m α) (msg : String := "input") : m Unit :=
 do it ← leftOver,
-   b ← lookahead $ catch (p *> pure ff) (λ _, pure tt),
+   b ← lookahead $ catch (p *> pure false) (λ _, pure true),
    if b then pure () else error msg Dlist.Empty it
 
 def eoi : m Unit :=
@@ -554,7 +554,7 @@ do it ← leftOver,
          | _                     := Result.ok [a] it none)
        (λ msg, pure $ match r with
            | Result.error msg' _ := if msg'.it.offset > msg.it.offset then r
-             else if msg.it.offset > msg'.it.offset then Result.error msg tt
+             else if msg.it.offset > msg'.it.offset then Result.error msg true
              else Result.error (merge msg msg') (msg.it.offset > it.offset)
            | _ := r))
     ((error "longestMatch: Empty List" : Parsec _ _) it),
diff --git a/library/init/lean/parser/syntax.lean b/library/init/lean/parser/syntax.lean
index 4f25d58f5f..b3301744b7 100644
--- a/library/init/lean/parser/syntax.lean
+++ b/library/init/lean/parser/syntax.lean
@@ -123,7 +123,7 @@ def kind : Syntax → Option SyntaxNodeKind
 
 def isOfKind (k : SyntaxNodeKind) : Syntax → Bool
 | (Syntax.rawNode n) := k.name = n.kind.name
-| _ := ff
+| _ := false
 
 section
 variables {m : Type → Type} [Monad m] (r : Syntax → m (Option Syntax))
diff --git a/library/init/lean/parser/term.lean b/library/init/lean/parser/term.lean
index 56d1b85889..c52a2be19a 100644
--- a/library/init/lean/parser/term.lean
+++ b/library/init/lean/parser/term.lean
@@ -41,7 +41,7 @@ node! «paren» ["(":maxPrec,
     special: nodeChoice! parenSpecial {
       /- Do not allow trailing comma. Looks a bit weird and would clash with
       adding support for tuple sections (https://downloads.haskell.org/~ghc/8.2.1/docs/html/usersGuide/glasgowExts.html#tuple-sections). -/
-      tuple: node! tuple [", ", tail: sepBy (Term.Parser 0) (symbol ", ") ff],
+      tuple: node! tuple [", ", tail: sepBy (Term.Parser 0) (symbol ", ") false],
       typed: node! typed [" : ", type: Term.Parser],
     }?,
   ]?,
@@ -282,14 +282,14 @@ node! «show» [
 def match.Parser : termParser :=
 node! «match» [
   "match ",
-  scrutinees: sepBy1 Term.Parser (symbol ", ") ff,
+  scrutinees: sepBy1 Term.Parser (symbol ", ") false,
   type: optType.Parser,
   " with ",
   optBar: (symbol " | ")?,
   equations: sepBy1
     node! «matchEquation» [
-      lhs: sepBy1 Term.Parser (symbol ", ") ff, ":=", rhs: Term.Parser]
-    (symbol " | ") ff,
+      lhs: sepBy1 Term.Parser (symbol ", ") false, ":=", rhs: Term.Parser]
+    (symbol " | ") false,
 ]
 
 @[derive Parser.HasTokens Parser.HasView]
diff --git a/library/init/lean/parser/token.lean b/library/init/lean/parser/token.lean
index 29494d9680..f50fd0e6ab 100644
--- a/library/init/lean/parser/token.lean
+++ b/library/init/lean/parser/token.lean
@@ -92,7 +92,7 @@ let ss : Substring := ⟨start, stop⟩ in
 Syntax.atom ⟨some {leading := ⟨start, start⟩, pos := start.offset, trailing := ⟨stop, stop⟩}, ss.toString⟩
 
 /-- Match an arbitrary Parser and return the consumed String in a `Syntax.atom`. -/
-@[inline] def raw {α : Type} (p : m α) (trailingWs := ff) : Parser := do
+@[inline] def raw {α : Type} (p : m α) (trailingWs := false) : Parser := do
   start ← leftOver,
   p,
   stop ← leftOver,
@@ -108,7 +108,7 @@ instance raw.view {α} (p : m α) (t) : Parser.HasView (Option SyntaxAtom) (raw
 
 /-- Like `raw (str s)`, but default to `s` in views. -/
 @[inline, derive HasTokens HasView]
-def rawStr (s : String) (trailingWs := ff) : Parser :=
+def rawStr (s : String) (trailingWs := false) : Parser :=
 raw (str s) trailingWs
 
 instance rawStr.viewDefault (s) (t) : Parser.HasViewDefault (rawStr s t : Parser) (Option SyntaxAtom) (some {val := s}) :=
diff --git a/library/init/lean/position.lean b/library/init/lean/position.lean
index 167cfd5636..d4c8589b97 100644
--- a/library/init/lean/position.lean
+++ b/library/init/lean/position.lean
@@ -43,7 +43,7 @@ namespace FileMap
 private def fromStringAux : Nat → String.Iterator → Nat → List (Nat × Nat)
 | 0     it line := []
 | (k+1) it line :=
-  if it.hasNext = ff then []
+  if it.hasNext = false then []
   else match it.curr with
        | '\n'  := (it.next.offset, line+1) :: fromStringAux k it.next (line+1)
        | other := fromStringAux k it.next line
diff --git a/library/init/lean/trace.lean b/library/init/lean/trace.lean
index 162da6088e..14b4462002 100644
--- a/library/init/lean/trace.lean
+++ b/library/init/lean/trace.lean
@@ -50,7 +50,7 @@ traceCtx cls msg (pure () : m Unit)
 instance (m) [Monad m] : MonadTracer (TraceT m) :=
 { traceRoot := λ α pos cls msg ctx, do {
     st ← get,
-    if st.opts.getBool cls = some tt then do {
+    if st.opts.getBool cls = some true then do {
       modify $ λ st, {curPos := pos, curTraces := [], ..st},
       a ← ctx.get,
       modify $ λ (st : TraceState), {roots := st.roots.insert pos ⟨msg, st.curTraces⟩, ..st},
@@ -62,7 +62,7 @@ instance (m) [Monad m] : MonadTracer (TraceT m) :=
     -- tracing enabled?
     some _ ← pure st.curPos | ctx.get,
     -- Trace class enabled?
-    if st.opts.getBool cls = some tt then do {
+    if st.opts.getBool cls = some true then do {
       put {curTraces := [], ..st},
       a ← ctx.get,
       modify $ λ (st' : TraceState), {curTraces := st.curTraces ++ [⟨msg, st'.curTraces⟩], ..st'},
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index ae9b183e2d..8fc2a703ef 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -172,7 +172,7 @@ void parser::scan() {
 }
 
 expr parser::mk_sorry(pos_info const & p, bool synthetic) {
-    return save_pos(::lean::mk_app(mk_constant(get_sorry_ax_name()), mk_expr_placeholder(), synthetic ? mk_bool_tt() : mk_bool_ff()), p);
+    return save_pos(::lean::mk_app(mk_constant(get_sorry_ax_name()), mk_expr_placeholder(), synthetic ? mk_bool_true() : mk_bool_false()), p);
 }
 
 void parser::updt_options() {
diff --git a/src/library/constants.cpp b/src/library/constants.cpp
index 1b4180b5b4..70f127f1e7 100644
--- a/src/library/constants.cpp
+++ b/src/library/constants.cpp
@@ -20,8 +20,8 @@ name const * g_bin_tree_empty = nullptr;
 name const * g_bin_tree_leaf = nullptr;
 name const * g_bin_tree_node = nullptr;
 name const * g_bool = nullptr;
-name const * g_bool_ff = nullptr;
-name const * g_bool_tt = nullptr;
+name const * g_bool_false = nullptr;
+name const * g_bool_true = nullptr;
 name const * g_combinator_k = nullptr;
 name const * g_cast = nullptr;
 name const * g_char = nullptr;
@@ -304,8 +304,8 @@ void initialize_constants() {
     g_bin_tree_leaf = new name{"BinTree", "leaf"};
     g_bin_tree_node = new name{"BinTree", "Node"};
     g_bool = new name{"Bool"};
-    g_bool_ff = new name{"Bool", "ff"};
-    g_bool_tt = new name{"Bool", "tt"};
+    g_bool_false = new name{"Bool", "false"};
+    g_bool_true = new name{"Bool", "true"};
     g_combinator_k = new name{"Combinator", "K"};
     g_cast = new name{"cast"};
     g_char = new name{"Char"};
@@ -589,8 +589,8 @@ void finalize_constants() {
     delete g_bin_tree_leaf;
     delete g_bin_tree_node;
     delete g_bool;
-    delete g_bool_ff;
-    delete g_bool_tt;
+    delete g_bool_false;
+    delete g_bool_true;
     delete g_combinator_k;
     delete g_cast;
     delete g_char;
@@ -873,8 +873,8 @@ name const & get_bin_tree_empty_name() { return *g_bin_tree_empty; }
 name const & get_bin_tree_leaf_name() { return *g_bin_tree_leaf; }
 name const & get_bin_tree_node_name() { return *g_bin_tree_node; }
 name const & get_bool_name() { return *g_bool; }
-name const & get_bool_ff_name() { return *g_bool_ff; }
-name const & get_bool_tt_name() { return *g_bool_tt; }
+name const & get_bool_false_name() { return *g_bool_false; }
+name const & get_bool_true_name() { return *g_bool_true; }
 name const & get_combinator_k_name() { return *g_combinator_k; }
 name const & get_cast_name() { return *g_cast; }
 name const & get_char_name() { return *g_char; }
diff --git a/src/library/constants.h b/src/library/constants.h
index 02f06b7443..7b8612c4af 100644
--- a/src/library/constants.h
+++ b/src/library/constants.h
@@ -22,8 +22,8 @@ name const & get_bin_tree_empty_name();
 name const & get_bin_tree_leaf_name();
 name const & get_bin_tree_node_name();
 name const & get_bool_name();
-name const & get_bool_ff_name();
-name const & get_bool_tt_name();
+name const & get_bool_false_name();
+name const & get_bool_true_name();
 name const & get_combinator_k_name();
 name const & get_cast_name();
 name const & get_char_name();
diff --git a/src/library/constants.txt b/src/library/constants.txt
index 1d605df968..adaa2b084b 100644
--- a/src/library/constants.txt
+++ b/src/library/constants.txt
@@ -15,8 +15,8 @@ BinTree.Empty
 BinTree.leaf
 BinTree.Node
 Bool
-Bool.ff
-Bool.tt
+Bool.false
+Bool.true
 Combinator.K
 cast
 Char
diff --git a/src/library/sorry.cpp b/src/library/sorry.cpp
index 2e3fc6159f..5b6d1f7efb 100644
--- a/src/library/sorry.cpp
+++ b/src/library/sorry.cpp
@@ -15,7 +15,7 @@ Author: Leonardo de Moura
 namespace lean {
 expr mk_sorry(abstract_type_context & ctx, expr const & ty, bool synthetic) {
     level u = get_level(ctx, ty);
-    return mk_app(mk_constant(get_sorry_ax_name(), levels(u)), ty, synthetic ? mk_bool_tt() : mk_bool_ff());
+    return mk_app(mk_constant(get_sorry_ax_name(), levels(u)), ty, synthetic ? mk_bool_true() : mk_bool_false());
 }
 
 bool is_sorry(expr const & e) {
@@ -26,7 +26,7 @@ bool is_synthetic_sorry(expr const & e) {
     if (!is_sorry(e)) return false;
     buffer<expr> args;
     get_app_args(e, args);
-    return is_constant(args[1], get_bool_tt_name());
+    return is_constant(args[1], get_bool_true_name());
 }
 
 bool has_synthetic_sorry(expr const & ex) {
diff --git a/src/library/util.cpp b/src/library/util.cpp
index 60f238243f..cbecb0cacc 100644
--- a/src/library/util.cpp
+++ b/src/library/util.cpp
@@ -964,25 +964,25 @@ expr infer_implicit_params(expr const & type, unsigned nparams, implicit_infer_k
 }
 
 static expr * g_bool = nullptr;
-static expr * g_bool_tt = nullptr;
-static expr * g_bool_ff = nullptr;
+static expr * g_bool_true = nullptr;
+static expr * g_bool_false = nullptr;
 
 void initialize_bool() {
     g_bool = new expr(mk_constant(get_bool_name()));
-    g_bool_ff = new expr(mk_constant(get_bool_ff_name()));
-    g_bool_tt = new expr(mk_constant(get_bool_tt_name()));
+    g_bool_false = new expr(mk_constant(get_bool_false_name()));
+    g_bool_true = new expr(mk_constant(get_bool_true_name()));
 }
 
 void finalize_bool() {
     delete g_bool;
-    delete g_bool_ff;
-    delete g_bool_tt;
+    delete g_bool_false;
+    delete g_bool_true;
 }
 
 expr mk_bool() { return *g_bool; }
-expr mk_bool_tt() { return *g_bool_tt; }
-expr mk_bool_ff() { return *g_bool_ff; }
-expr to_bool_expr(bool b) { return b ? mk_bool_tt() : mk_bool_ff(); }
+expr mk_bool_true() { return *g_bool_true; }
+expr mk_bool_false() { return *g_bool_false; }
+expr to_bool_expr(bool b) { return b ? mk_bool_true() : mk_bool_false(); }
 
 name get_dep_recursor(environment const &, name const & n) {
     return name(n, g_rec);
diff --git a/src/library/util.h b/src/library/util.h
index c147494f79..a628f741af 100644
--- a/src/library/util.h
+++ b/src/library/util.h
@@ -267,8 +267,8 @@ expr mk_nary_app(expr const & op, buffer<expr> const & nary_args);
 expr mk_nary_app(expr const & op, unsigned num_nary_args, expr const * nary_args);
 
 expr mk_bool();
-expr mk_bool_tt();
-expr mk_bool_ff();
+expr mk_bool_true();
+expr mk_bool_false();
 expr to_bool_expr(bool b);
 
 /* Similar to is_head_beta, but ignores annotations around the function. */