diff --git a/tests/lean/973b.lean b/tests/lean/973b.lean
index 59c2bb5559..ad1a17f1f4 100644
--- a/tests/lean/973b.lean
+++ b/tests/lean/973b.lean
@@ -1,5 +1,5 @@
-constant f : Nat → Nat
-constant q : Nat → (Nat → Prop) → Nat
+opaque f : Nat → Nat
+opaque q : Nat → (Nat → Prop) → Nat
 
 @[simp]
 theorem ex {x : Nat} {p : Nat → Prop} (h₁ : p x) (h₂ : q x p = x) : f x = x :=
diff --git a/tests/lean/PPInstances.lean b/tests/lean/PPInstances.lean
index 00c2a1db1c..c4ffea1777 100644
--- a/tests/lean/PPInstances.lean
+++ b/tests/lean/PPInstances.lean
@@ -19,8 +19,8 @@ instance NormedField.toRing [instNF : NormedField α] : Ring α := { add := inst
 
 instance SemiNormedSpace.toModule [NormedField α] [SemiNormedGroup β] [SemiNormedSpace α β] : Module α β := {}
 
-constant R : Type := Unit
-constant foo (a b : R) : R := a
+opaque R : Type := Unit
+opaque foo (a b : R) : R := a
 
 instance R.NormedField : NormedField R := { add := foo, add_comm := sorry }
 instance R.Ring : Ring R := { add := foo }
diff --git a/tests/lean/Reformat.lean.expected.out b/tests/lean/Reformat.lean.expected.out
index 7a7c828c63..16a37c1125 100644
--- a/tests/lean/Reformat.lean.expected.out
+++ b/tests/lean/Reformat.lean.expected.out
@@ -110,14 +110,14 @@ theorem congrArg {α : Sort u} {β : Sort v} {a₁ a₂ : α} (f : α → β) (h
 /-
 Initialize the Quotient Module, which effectively adds the following definitions:
 
-constant Quot {α : Sort u} (r : α → α → Prop) : Sort u
+opaque Quot {α : Sort u} (r : α → α → Prop) : Sort u
 
-constant Quot.mk {α : Sort u} (r : α → α → Prop) (a : α) : Quot r
+opaque Quot.mk {α : Sort u} (r : α → α → Prop) (a : α) : Quot r
 
-constant Quot.lift {α : Sort u} {r : α → α → Prop} {β : Sort v} (f : α → β) :
+opaque Quot.lift {α : Sort u} {r : α → α → Prop} {β : Sort v} (f : α → β) :
   (∀ a b : α, r a b → Eq (f a) (f b)) → Quot r → β
 
-constant Quot.ind {α : Sort u} {r : α → α → Prop} {β : Quot r → Prop} :
+opaque Quot.ind {α : Sort u} {r : α → α → Prop} {β : Quot r → Prop} :
   (∀ a : α, β (Quot.mk r a)) → ∀ q : Quot r, β q
 -/
 init_quot
@@ -212,7 +212,7 @@ theorem neTrueOfEqFalse : {b : Bool} → Eq b false → Not (Eq b true)
 class Inhabited (α : Sort u) :=
   (default : α)
 
-constant arbitrary (α : Sort u) [s : Inhabited α] : α :=
+opaque arbitrary (α : Sort u) [s : Inhabited α] : α :=
   @Inhabited.default α s
 
 instance (α : Sort u) {β : Sort v} [Inhabited β] : Inhabited (α → β) :=
@@ -316,4 +316,3 @@ instance {α : Type u} [DecidableEq α] : BEq α :=
 @[macroInline]
 def dite {α : Sort u} (c : Prop) [h : Decidable c] (t : c → α) (e : Not c → α) : α :=
   Decidable.casesOn (motive := fun _ => α) h e t
-
diff --git a/tests/lean/Reformat/Input.lean b/tests/lean/Reformat/Input.lean
index 2d4ea741ea..deb4838c36 100644
--- a/tests/lean/Reformat/Input.lean
+++ b/tests/lean/Reformat/Input.lean
@@ -92,14 +92,14 @@ theorem congrArg {α : Sort u} {β : Sort v} {a₁ a₂ : α} (f : α → β) (h
 /-
 Initialize the Quotient Module, which effectively adds the following definitions:
 
-constant Quot {α : Sort u} (r : α → α → Prop) : Sort u
+opaque Quot {α : Sort u} (r : α → α → Prop) : Sort u
 
-constant Quot.mk {α : Sort u} (r : α → α → Prop) (a : α) : Quot r
+opaque Quot.mk {α : Sort u} (r : α → α → Prop) (a : α) : Quot r
 
-constant Quot.lift {α : Sort u} {r : α → α → Prop} {β : Sort v} (f : α → β) :
+opaque Quot.lift {α : Sort u} {r : α → α → Prop} {β : Sort v} (f : α → β) :
   (∀ a b : α, r a b → Eq (f a) (f b)) → Quot r → β
 
-constant Quot.ind {α : Sort u} {r : α → α → Prop} {β : Quot r → Prop} :
+opaque Quot.ind {α : Sort u} {r : α → α → Prop} {β : Quot r → Prop} :
   (∀ a : α, β (Quot.mk r a)) → ∀ q : Quot r, β q
 -/
 init_quot
@@ -183,7 +183,7 @@ theorem neTrueOfEqFalse : {b : Bool} → Eq b false → Not (Eq b true)
 class Inhabited (α : Sort u) :=
   (default : α)
 
-constant arbitrary (α : Sort u) [s : Inhabited α] : α :=
+opaque arbitrary (α : Sort u) [s : Inhabited α] : α :=
   @Inhabited.default α s
 
 instance (α : Sort u) {β : Sort v} [Inhabited β] : Inhabited (α → β) := {
diff --git a/tests/lean/consumePPHint.lean b/tests/lean/consumePPHint.lean
index 4a3b50ae70..0ea876dd48 100644
--- a/tests/lean/consumePPHint.lean
+++ b/tests/lean/consumePPHint.lean
@@ -1,5 +1,5 @@
-constant p : Nat → Prop
-constant q : Nat → Prop
+opaque p : Nat → Prop
+opaque q : Nat → Prop
 
 theorem p_of_q : q x → p x := sorry
 
diff --git a/tests/lean/interactive/hover.lean b/tests/lean/interactive/hover.lean
index 07ccc44708..cc46a372e0 100644
--- a/tests/lean/interactive/hover.lean
+++ b/tests/lean/interactive/hover.lean
@@ -103,15 +103,15 @@ example : Id Nat := do
   n
 
 
-constant foo : Nat
+opaque foo : Nat
 
 #check _root_.foo
        --^ textDocument/hover
 
 namespace Bar
 
-constant foo : Nat
-       --^ textDocument/hover
+opaque foo : Nat
+     --^ textDocument/hover
 
 #check _root_.foo
        --^ textDocument/hover
diff --git a/tests/lean/linterUnusedVariables.lean b/tests/lean/linterUnusedVariables.lean
index e664bc6925..c549eb6d43 100644
--- a/tests/lean/linterUnusedVariables.lean
+++ b/tests/lean/linterUnusedVariables.lean
@@ -179,8 +179,8 @@ register_option opt : Nat := {
 }
 
 
-constant foo (x : Nat) : Nat
-constant foo' (x : Nat) : Nat :=
+opaque foo (x : Nat) : Nat
+opaque foo' (x : Nat) : Nat :=
   let y := 5
   3
 variable (bar)
@@ -201,7 +201,7 @@ def externDef (x : Nat) : Nat :=
   5
 
 @[extern "test"]
-constant externConst (x : Nat) : Nat :=
+opaque externConst (x : Nat) : Nat :=
   let y := 3
   5
 
diff --git a/tests/lean/multiConstantError.lean b/tests/lean/multiConstantError.lean
index bd7a90314c..42aeda8a0d 100644
--- a/tests/lean/multiConstantError.lean
+++ b/tests/lean/multiConstantError.lean
@@ -1,3 +1,3 @@
-constant a b c : Nat
+opaque a b c : Nat
 
-constant a α β : β → Bool
+opaque a α β : β → Bool
diff --git a/tests/lean/run/1385.lean b/tests/lean/run/1385.lean
index 5ee3c949c9..dffa4d1d3c 100644
--- a/tests/lean/run/1385.lean
+++ b/tests/lean/run/1385.lean
@@ -1,5 +1,5 @@
 def S := List Nat
-constant TSpec : NonemptyType
+opaque TSpec : NonemptyType
 def T (s : S) : Type :=  TSpec.type
 instance (s : S) : Nonempty (T s) :=
   TSpec.property
diff --git a/tests/lean/run/335.lean b/tests/lean/run/335.lean
index e2515ac48b..396f55ab8f 100644
--- a/tests/lean/run/335.lean
+++ b/tests/lean/run/335.lean
@@ -1,5 +1,5 @@
-constant foo : {x : Nat} → Type
-constant bar : {T : Type} → ({x : T} → Type) → Type
+opaque foo : {x : Nat} → Type
+opaque bar : {T : Type} → ({x : T} → Type) → Type
 structure Baz where
   baz : {x : Nat} → Type
 
diff --git a/tests/lean/run/470_lean3.lean b/tests/lean/run/470_lean3.lean
index aa6269dea8..fe42fd0bd4 100644
--- a/tests/lean/run/470_lean3.lean
+++ b/tests/lean/run/470_lean3.lean
@@ -2,6 +2,6 @@ section foo
 
 axiom foo : Type
 
-constant bla : Nat
+opaque bla : Nat
 
 end foo
diff --git a/tests/lean/run/602.lean b/tests/lean/run/602.lean
index 2a564734a3..f71fe9e02d 100644
--- a/tests/lean/run/602.lean
+++ b/tests/lean/run/602.lean
@@ -21,8 +21,8 @@ instance NormedField.toRing [instNF : NormedField α] : Ring α := { add := inst
 -- @[inferTCGoalsRL]
 instance SemiNormedSpace.toModule [NormedField α] [SemiNormedGroup β] [SemiNormedSpace α β] : Module α β := {}
 
-constant R : Type := Unit
-constant foo (a b : R) : R := a
+opaque R : Type := Unit
+opaque foo (a b : R) : R := a
 
 instance R.NormedField : NormedField R := { add := foo, add_comm := sorry }
 instance R.Ring : Ring R := { add := foo }
diff --git a/tests/lean/run/988.lean b/tests/lean/run/988.lean
index 5bbae82825..5fabf5bea8 100644
--- a/tests/lean/run/988.lean
+++ b/tests/lean/run/988.lean
@@ -6,7 +6,7 @@ def empty : Fin 0 → Nat := (nomatch ·)
 theorem append_empty (x : Fin i → Nat) : x ++ empty = x :=
   funext fun i => dif_pos _
 
-constant f : (Fin 0 → Nat) → Prop
+opaque f : (Fin 0 → Nat) → Prop
 example : f (empty ++ empty) = f empty := by simp only [append_empty] -- should work
 
 @[congr] theorem Array.get_congr (as bs : Array α) (h : as = bs) (i : Fin as.size) (j : Nat) (hi : i = j) :
diff --git a/tests/lean/run/KyleAlg.lean b/tests/lean/run/KyleAlg.lean
index 4237febb3b..30ad6aaecc 100644
--- a/tests/lean/run/KyleAlg.lean
+++ b/tests/lean/run/KyleAlg.lean
@@ -246,7 +246,7 @@ where
       | _ => return ()
 
 @[implementedBy Expr.dagSizeUnsafe]
-constant Expr.dagSize (e : Expr) : IO Nat
+opaque Expr.dagSize (e : Expr) : IO Nat
 
 def getDeclTypeValueDagSize (declName : Name) : CoreM Nat := do
   let info ← getConstInfo declName
diff --git a/tests/lean/run/MonadControl_tutorial.lean b/tests/lean/run/MonadControl_tutorial.lean
index f7f29d5bfe..d2bef98630 100644
--- a/tests/lean/run/MonadControl_tutorial.lean
+++ b/tests/lean/run/MonadControl_tutorial.lean
@@ -7,8 +7,8 @@ def σ := Nat
 @[reducible]
 def β := String
 
-constant foo : ∀ {α}, IO α → IO α
-constant bar : StateT σ IO β
+opaque foo : ∀ {α}, IO α → IO α
+opaque bar : StateT σ IO β
 
 def mapped_foo : StateT σ IO β := do
   let s ← get
diff --git a/tests/lean/run/autoboundIssues.lean b/tests/lean/run/autoboundIssues.lean
index 2c2579a600..1e88b98747 100644
--- a/tests/lean/run/autoboundIssues.lean
+++ b/tests/lean/run/autoboundIssues.lean
@@ -4,7 +4,7 @@ example : n.succ = 1 → n = 0 := by
 example (h : n.succ = 1) : n = 0 := by
   injection h; assumption
 
-constant T : Type
-constant T.Pred : T → T → Prop
+opaque T : Type
+opaque T.Pred : T → T → Prop
 
 example {ρ} (hρ : ρ.Pred σ) : T.Pred ρ ρ := sorry
diff --git a/tests/lean/run/etaStruct.lean b/tests/lean/run/etaStruct.lean
index 0510337515..ebee4062c8 100644
--- a/tests/lean/run/etaStruct.lean
+++ b/tests/lean/run/etaStruct.lean
@@ -64,8 +64,8 @@ example (x : Nat × Nat) : (frob x).2 = 42 := rfl
 
 example (x y : Unit) : x = y := rfl
 
-constant f : Nat → Unit
-constant g : Nat → Unit
+opaque f : Nat → Unit
+opaque g : Nat → Unit
 
 example (x y : Nat) : f x = f y := rfl
 
diff --git a/tests/lean/run/fun.lean b/tests/lean/run/fun.lean
index 7c12fb5262..d265e0baa8 100644
--- a/tests/lean/run/fun.lean
+++ b/tests/lean/run/fun.lean
@@ -1,15 +1,15 @@
 open Function Bool
 
 
-constant f : Nat → Bool := default
-constant g : Nat → Nat := default
+opaque f : Nat → Bool := default
+opaque g : Nat → Nat := default
 
 #check f ∘ g ∘ g
 
 #check (id : Nat → Nat)
 
-constant h : Nat → Bool → Nat := default
+opaque h : Nat → Bool → Nat := default
 
 
-constant f1 : Nat → Nat → Bool := default
-constant f2 : Bool → Nat := default
+opaque f1 : Nat → Nat → Bool := default
+opaque f2 : Bool → Nat := default
diff --git a/tests/lean/run/isDefEqIssue.lean b/tests/lean/run/isDefEqIssue.lean
index 1a7c9e9726..932a859539 100644
--- a/tests/lean/run/isDefEqIssue.lean
+++ b/tests/lean/run/isDefEqIssue.lean
@@ -1,4 +1,4 @@
-constant getA (s : String) : Array String := #[]
+opaque getA (s : String) : Array String := #[]
 
 private def resolveLValAux (s : String) (i : Nat) : Nat :=
   let s1 := s
diff --git a/tests/lean/run/lean3_zulip_issues_1.lean b/tests/lean/run/lean3_zulip_issues_1.lean
index 9e9cad5693..108f99b7d9 100644
--- a/tests/lean/run/lean3_zulip_issues_1.lean
+++ b/tests/lean/run/lean3_zulip_issues_1.lean
@@ -40,7 +40,7 @@ inductive Vec.{u} (α : Type u) : Nat → Type u
   | nil  : Vec α 0
   | cons : α → {n : Nat} → Vec α n → Vec α (Nat.succ n) -- TODO: investigate why +1 doesn't work here
 
-constant Vars : Type
+opaque Vars : Type
 
 structure Lang :=
   (funcs : Nat → Type)
diff --git a/tests/lean/run/new_inductive.lean b/tests/lean/run/new_inductive.lean
index 1283e04f63..28db0848a9 100644
--- a/tests/lean/run/new_inductive.lean
+++ b/tests/lean/run/new_inductive.lean
@@ -56,7 +56,7 @@ inductive Rbnode (α : Type u)
 namespace Rbnode
 variable {α : Type u}
 
-constant insert (lt : α → α → Prop) [DecidableRel lt] (t : Rbnode α) (x : α) : Rbnode α := Rbnode.leaf
+opaque insert (lt : α → α → Prop) [DecidableRel lt] (t : Rbnode α) (x : α) : Rbnode α := Rbnode.leaf
 
 inductive WellFormed (lt : α → α → Prop) : Rbnode α → Prop
 | leafWff : WellFormed lt leaf
diff --git a/tests/lean/run/openInScopeBug.lean b/tests/lean/run/openInScopeBug.lean
index fe8fc4f663..b1498aab4c 100644
--- a/tests/lean/run/openInScopeBug.lean
+++ b/tests/lean/run/openInScopeBug.lean
@@ -1,5 +1,5 @@
-constant f : Nat → Nat
-constant g : Nat → Nat
+opaque f : Nat → Nat
+opaque g : Nat → Nat
 
 namespace Foo
 
diff --git a/tests/lean/run/rossel1.lean b/tests/lean/run/rossel1.lean
index 319403caf4..a62747d956 100644
--- a/tests/lean/run/rossel1.lean
+++ b/tests/lean/run/rossel1.lean
@@ -1,4 +1,4 @@
-constant ID : Type
+opaque ID : Type
 
 -- A `Reactor` contains "things" identified by an `ID`. It also contains other `Reactor`s, thereby giving us a tree structure of reactors.
 inductive Reactor
diff --git a/tests/lean/run/simp3.lean b/tests/lean/run/simp3.lean
index 924b5497bf..3e59f0bfec 100644
--- a/tests/lean/run/simp3.lean
+++ b/tests/lean/run/simp3.lean
@@ -1,11 +1,11 @@
-constant f (x : Nat) : Nat
+opaque f (x : Nat) : Nat
 @[simp] axiom fEq (x : Nat) : f x = x
 
 theorem ex1 (x : Nat) : f (f x, x).fst = x := by simp
 
 theorem ex2 (x : Nat) : f ((fun a => f (f a)) x) = x := by simp
 
-constant g (x : Nat) : Nat
+opaque g (x : Nat) : Nat
 @[simp] axiom gEq (x : Nat) : g x = match x with | 0 => 1 | x+1 => 2
 @[simp] theorem add1 (x : Nat) : x + 1 = x.succ := rfl
 
diff --git a/tests/lean/run/simp4.lean b/tests/lean/run/simp4.lean
index 30352a58b4..60528b6c4d 100644
--- a/tests/lean/run/simp4.lean
+++ b/tests/lean/run/simp4.lean
@@ -1,6 +1,6 @@
-constant f : Nat → Nat
-constant q : Nat → Prop
-constant r : Nat → Prop
+opaque f : Nat → Nat
+opaque q : Nat → Prop
+opaque r : Nat → Prop
 
 @[simp] axiom ax1 (p : Prop) : (p ∧ True) ↔ p
 @[simp] axiom ax2 (x : Nat) : q (f x)
diff --git a/tests/lean/run/simpInv.lean b/tests/lean/run/simpInv.lean
index 61f8dc9082..dee2465f98 100644
--- a/tests/lean/run/simpInv.lean
+++ b/tests/lean/run/simpInv.lean
@@ -1,13 +1,13 @@
-constant g (x y : Nat) : Nat
-constant f (x y : Nat) : Nat
+opaque g (x y : Nat) : Nat
+opaque f (x y : Nat) : Nat
 axiom f_def (x y : Nat) : f x y = g x y
 axiom f_ax (x : Nat) : f x x = x
 
 theorem ex1 (x : Nat) : g x x = x := by
   simp [← f_def, f_ax]
 
-constant p (x y : Nat) : Prop
-constant q (x y : Nat) : Prop
+opaque p (x y : Nat) : Prop
+opaque q (x y : Nat) : Prop
 axiom p_def (x y : Nat) : p x y ↔ q x y
 axiom p_ax (x : Nat) : p x x
 
diff --git a/tests/lean/run/simpPrio.lean b/tests/lean/run/simpPrio.lean
index d005414fbb..373e727a72 100644
--- a/tests/lean/run/simpPrio.lean
+++ b/tests/lean/run/simpPrio.lean
@@ -1,4 +1,4 @@
-constant n : Nat
+opaque n : Nat
 @[simp] axiom prio_1000 : n = 1000
 @[simp 10] axiom prio_10 : n = 10
 -- simp should prefer the prio_1000 lemma with the higher priority
diff --git a/tests/lean/run/simpStar.lean b/tests/lean/run/simpStar.lean
index c44dc2783d..7ef9d42a1e 100644
--- a/tests/lean/run/simpStar.lean
+++ b/tests/lean/run/simpStar.lean
@@ -1,5 +1,5 @@
-constant f (x y : Nat) : Nat
-constant g (x : Nat) : Nat
+opaque f (x y : Nat) : Nat
+opaque g (x : Nat) : Nat
 
 theorem ex1 (x : Nat) (h₁ : f x x = g x) (h₂ : g x = x) : f x (f x x) = x := by
   simp
diff --git a/tests/lean/run/typeAscImp.lean b/tests/lean/run/typeAscImp.lean
index 8b25de924f..4322b0e935 100644
--- a/tests/lean/run/typeAscImp.lean
+++ b/tests/lean/run/typeAscImp.lean
@@ -1,7 +1,7 @@
 def Ctx := String → Type
 abbrev State (Γ : Ctx) := {x : String} → Γ x
 
-constant p {Γ : Ctx} (s : State Γ) : Prop
+opaque p {Γ : Ctx} (s : State Γ) : Prop
 
 theorem ex {Γ : Ctx} (s : State Γ) (h : (a : State Γ) → @p Γ a) : @p Γ s :=
   h ‹_›
diff --git a/tests/lean/sanitychecks.lean b/tests/lean/sanitychecks.lean
index 1cc6f5a59d..33ed41a6cd 100644
--- a/tests/lean/sanitychecks.lean
+++ b/tests/lean/sanitychecks.lean
@@ -7,7 +7,7 @@ partial theorem unsound2 : False := -- Error
 unsafe theorem unsound3 : False := -- Error
   unsound3
 
-constant unsound4 : False  -- Error
+opaque unsound4 : False  -- Error
 
 axiom magic : False -- OK
 namespace Foo
diff --git a/tests/lean/simpDisch.lean b/tests/lean/simpDisch.lean
index fd3df0c13c..6acd918764 100644
--- a/tests/lean/simpDisch.lean
+++ b/tests/lean/simpDisch.lean
@@ -1,4 +1,4 @@
-constant f : Nat → Nat
+opaque f : Nat → Nat
 @[simp] axiom fEq (x : Nat) (h : x ≠ 0) : f x = x
 
 example (x : Nat) (h : x ≠ 0) : f x = x + 0 := by
diff --git a/tests/lean/simpZetaFalse.lean b/tests/lean/simpZetaFalse.lean
index 8e26af76e6..bc17452d54 100644
--- a/tests/lean/simpZetaFalse.lean
+++ b/tests/lean/simpZetaFalse.lean
@@ -1,4 +1,4 @@
-constant f : Nat → Nat
+opaque f : Nat → Nat
 axiom f_eq (x : Nat) : f (f x) = x
 
 theorem ex1 (x : Nat) (h : f (f x) = x) : (let y := x*x; if f (f x) = x then 1 else y + 1) = 1 := by
diff --git a/tests/lean/smartUnfoldingMatch.lean b/tests/lean/smartUnfoldingMatch.lean
index d52f2bb3ff..11c5d74770 100644
--- a/tests/lean/smartUnfoldingMatch.lean
+++ b/tests/lean/smartUnfoldingMatch.lean
@@ -6,7 +6,7 @@ elab "whnf%" t:term : term <= expectedType => do
   trace[Meta.debug] "r: {r}"
   return r
 
-constant x : Option Nat := some 42
+opaque x : Option Nat := some 42
 
 set_option trace.Meta.debug true
 #eval whnf% x.getD 0
diff --git a/tests/lean/unboxStruct.lean b/tests/lean/unboxStruct.lean
index 7b6fccb237..df57b1d66d 100644
--- a/tests/lean/unboxStruct.lean
+++ b/tests/lean/unboxStruct.lean
@@ -1,9 +1,8 @@
-
 structure AddrSpace where
   index : UInt32
 
 @[extern "foo"]
-constant foo (addrSpace : AddrSpace) : IO PUnit
+opaque foo (addrSpace : AddrSpace) : IO PUnit
 
 set_option trace.compiler.ir.result true in
 -- should accept and pass an unboxed `uint32`