chore: update stage0

stage0/src/Init/Control/Basic.lean

@@ -75,8 +75,8 @@ Suppose we have `foo : ∀ α, IO α → IO α` and `bar : StateT σ IO β` (ie,
 We might want to 'map' `bar` by `foo`. Concretely we would write this as:
 
 ```lean
-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

stage0/src/Init/Core.lean

@@ -1109,7 +1109,7 @@ namespace Lean
   If an extern function is executed, then the trusted code base will also include the implementation of the associated
   foreign function.
 -/
-constant reduceBool (b : Bool) : Bool := b
+opaque reduceBool (b : Bool) : Bool := b
 
 /--
   Similar to `Lean.reduceBool` for closed `Nat` terms.
@@ -1117,7 +1117,7 @@ constant reduceBool (b : Bool) : Bool := b
   Remark: we do not have plans for supporting a generic `reduceValue {α} (a : α) : α := a`.
   The main issue is that it is non-trivial to convert an arbitrary runtime object back into a Lean expression.
   We believe `Lean.reduceBool` enables most interesting applications (e.g., proof by reflection). -/
-constant reduceNat (n : Nat) : Nat := n
+opaque reduceNat (n : Nat) : Nat := n
 
 axiom ofReduceBool (a b : Bool) (h : reduceBool a = b) : a = b
 axiom ofReduceNat (a b : Nat) (h : reduceNat a = b)    : a = b

stage0/src/Init/Data/Float.lean

@@ -17,7 +17,7 @@ structure FloatSpec where
   decLe : DecidableRel le
 
 -- Just show FloatSpec is inhabited.
-constant floatSpec : FloatSpec := {
+opaque floatSpec : FloatSpec := {
   float := Unit,
   val   := (),
   lt    := fun _ _ => True,
@@ -31,11 +31,11 @@ structure Float where
 
 instance : Inhabited Float := ⟨{ val := floatSpec.val }⟩
 
-@[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
+@[extern "lean_float_add"]  opaque Float.add : Float → Float → Float
+@[extern "lean_float_sub"]  opaque Float.sub : Float → Float → Float
+@[extern "lean_float_mul"]  opaque Float.mul : Float → Float → Float
+@[extern "lean_float_div"]  opaque Float.div : Float → Float → Float
+@[extern "lean_float_negate"]   opaque Float.neg : Float → Float
 
 set_option bootstrap.genMatcherCode false
 def Float.lt  : Float → Float → Prop := fun a b =>
@@ -53,28 +53,28 @@ instance : Neg Float       := ⟨Float.neg⟩
 instance : LT Float        := ⟨Float.lt⟩
 instance : LE Float        := ⟨Float.le⟩
 
-@[extern "lean_float_beq"] constant Float.beq (a b : Float) : Bool
+@[extern "lean_float_beq"] opaque Float.beq (a b : Float) : Bool
 
 instance : BEq Float := ⟨Float.beq⟩
 
-@[extern "lean_float_decLt"]   constant Float.decLt (a b : Float) : Decidable (a < b) :=
+@[extern "lean_float_decLt"]   opaque Float.decLt (a b : Float) : Decidable (a < b) :=
   match a, b with
   | ⟨a⟩, ⟨b⟩ => floatSpec.decLt a b
 
-@[extern "lean_float_decLe"] constant Float.decLe (a b : Float) : Decidable (a ≤ b) :=
+@[extern "lean_float_decLe"] opaque Float.decLe (a b : Float) : Decidable (a ≤ b) :=
   match a, b with
   | ⟨a⟩, ⟨b⟩ => floatSpec.decLe a b
 
 instance floatDecLt (a b : Float) : Decidable (a < b) := Float.decLt a b
 instance floatDecLe (a b : Float) : Decidable (a ≤ b) := Float.decLe a b
 
-@[extern "lean_float_to_string"] constant Float.toString : Float → String
+@[extern "lean_float_to_string"] opaque Float.toString : Float → String
 
-@[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
+@[extern "lean_float_to_uint8"] opaque Float.toUInt8 : Float → UInt8
+@[extern "lean_float_to_uint16"] opaque Float.toUInt16 : Float → UInt16
+@[extern "lean_float_to_uint32"] opaque Float.toUInt32 : Float → UInt32
+@[extern "lean_float_to_uint64"] opaque Float.toUInt64 : Float → UInt64
+@[extern "lean_float_to_usize"] opaque Float.toUSize : Float → USize
 
 instance : ToString Float where
   toString := Float.toString
@@ -84,29 +84,29 @@ instance : Repr Float where
 
 instance : ReprAtom Float  := ⟨⟩
 
-@[extern "lean_uint64_to_float"] constant UInt64.toFloat (n : UInt64) : Float
+@[extern "lean_uint64_to_float"] opaque UInt64.toFloat (n : UInt64) : Float
 
-@[extern "sin"] constant Float.sin : Float → Float
-@[extern "cos"] constant Float.cos : Float → Float
-@[extern "tan"] constant Float.tan : Float → Float
-@[extern "asin"] constant Float.asin : Float → Float
-@[extern "acos"] constant Float.acos : Float → Float
-@[extern "atan"] constant Float.atan : Float → Float
-@[extern "atan2"] constant Float.atan2 : Float → Float → Float
-@[extern "sinh"] constant Float.sinh : Float → Float
-@[extern "cosh"] constant Float.cosh : Float → Float
-@[extern "tanh"] constant Float.tanh : Float → Float
-@[extern "asinh"] constant Float.asinh : Float → Float
-@[extern "acosh"] constant Float.acosh : Float → Float
-@[extern "atanh"] constant Float.atanh : Float → Float
-@[extern "exp"] constant Float.exp : Float → Float
-@[extern "exp2"] constant Float.exp2 : Float → Float
-@[extern "log"] constant Float.log : Float → Float
-@[extern "log2"] constant Float.log2 : Float → Float
-@[extern "log10"] constant Float.log10 : Float → Float
-@[extern "pow"] constant Float.pow : Float → Float → Float
-@[extern "sqrt"] constant Float.sqrt : Float → Float
-@[extern "cbrt"] constant Float.cbrt : Float → Float
+@[extern "sin"] opaque Float.sin : Float → Float
+@[extern "cos"] opaque Float.cos : Float → Float
+@[extern "tan"] opaque Float.tan : Float → Float
+@[extern "asin"] opaque Float.asin : Float → Float
+@[extern "acos"] opaque Float.acos : Float → Float
+@[extern "atan"] opaque Float.atan : Float → Float
+@[extern "atan2"] opaque Float.atan2 : Float → Float → Float
+@[extern "sinh"] opaque Float.sinh : Float → Float
+@[extern "cosh"] opaque Float.cosh : Float → Float
+@[extern "tanh"] opaque Float.tanh : Float → Float
+@[extern "asinh"] opaque Float.asinh : Float → Float
+@[extern "acosh"] opaque Float.acosh : Float → Float
+@[extern "atanh"] opaque Float.atanh : Float → Float
+@[extern "exp"] opaque Float.exp : Float → Float
+@[extern "exp2"] opaque Float.exp2 : Float → Float
+@[extern "log"] opaque Float.log : Float → Float
+@[extern "log2"] opaque Float.log2 : Float → Float
+@[extern "log10"] opaque Float.log10 : Float → Float
+@[extern "pow"] opaque Float.pow : Float → Float → Float
+@[extern "sqrt"] opaque Float.sqrt : Float → Float
+@[extern "cbrt"] opaque Float.cbrt : Float → Float
 
 instance : Pow Float Float := ⟨Float.pow⟩
 
@@ -114,4 +114,4 @@ instance : Pow Float Float := ⟨Float.pow⟩
 Efficiently computes `x * 2^i`.
 -/
 @[extern "lean_float_scaleb"]
-constant Float.scaleB (x : Float) (i : @& Int) : Float
+opaque Float.scaleB (x : Float) (i : @& Int) : Float

stage0/src/Init/Data/String/Extra.lean

@@ -23,10 +23,10 @@ def toNat! (s : String) : Nat :=
   Convert a UTF-8 encoded `ByteArray` string to `String`.
   The result is unspecified if `a` is not properly UTF-8 encoded. -/
 @[extern "lean_string_from_utf8_unchecked"]
-constant fromUTF8Unchecked (a : @& ByteArray) : String
+opaque fromUTF8Unchecked (a : @& ByteArray) : String
 
 @[extern "lean_string_to_utf8"]
-constant toUTF8 (a : @& String) : ByteArray
+opaque toUTF8 (a : @& String) : ByteArray
 
 theorem one_le_csize (c : Char) : 1 ≤ csize c := by
   simp [csize, Char.utf8Size]

stage0/src/Init/Meta.lean

@@ -23,16 +23,16 @@ private constant version.getPatch (u : Unit) : Nat
 def version.patch : Nat := version.getPatch ()
 
 @[extern "lean_get_githash"]
-constant getGithash (u : Unit) : String
+opaque getGithash (u : Unit) : String
 def githash : String := getGithash ()
 
 @[extern c inline "LEAN_VERSION_IS_RELEASE"]
-constant version.getIsRelease (u : Unit) : Bool
+opaque version.getIsRelease (u : Unit) : Bool
 def version.isRelease : Bool := version.getIsRelease ()
 
 /-- Additional version description like "nightly-2018-03-11" -/
 @[extern c inline "lean_mk_string(LEAN_SPECIAL_VERSION_DESC)"]
-constant version.getSpecialDesc (u : Unit) : String
+opaque version.getSpecialDesc (u : Unit) : String
 def version.specialDesc : String := version.getSpecialDesc ()
 
 def versionStringCore :=
@@ -61,7 +61,7 @@ def toolchain :=
     ""
 
 @[extern c inline "LEAN_IS_STAGE0"]
-constant Internal.isStage0 (u : Unit) : Bool
+opaque Internal.isStage0 (u : Unit) : Bool
 
 /- Valid identifier names -/
 def isGreek (c : Char) : Bool :=

stage0/src/Init/Prelude.lean

@@ -89,14 +89,14 @@ theorem congrFun {α : Sort u} {β : α → Sort v} {f g : (x : α) →  β x} (
 /-
 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
@@ -795,7 +795,7 @@ protected def Nat.sub : (@& Nat) → (@& Nat) → Nat
 instance : Sub Nat where
   sub := Nat.sub
 
-@[extern "lean_system_platform_nbits"] constant System.Platform.getNumBits : Unit → Subtype fun (n : Nat) => Or (Eq n 32) (Eq n 64) :=
+@[extern "lean_system_platform_nbits"] opaque System.Platform.getNumBits : Unit → Subtype fun (n : Nat) => Or (Eq n 32) (Eq n 64) :=
   fun _ => ⟨64, Or.inr rfl⟩ -- inhabitant
 
 def System.Platform.numBits : Nat :=
@@ -1207,7 +1207,7 @@ unsafe def unsafeCast {α : Type u} {β : Type v} (a : α) : β :=
   ULift.down.{max u v} (cast lcProof (ULift.up.{max u v} a))
 
 @[neverExtract, extern "lean_panic_fn"]
-constant panicCore {α : Type u} [Inhabited α] (msg : String) : α
+opaque panicCore {α : Type u} [Inhabited α] (msg : String) : α
 
 /-
   This is workaround for `panic` occurring in monadic code. See issue #695.
@@ -1714,16 +1714,16 @@ class Hashable (α : Sort u) where
 export Hashable (hash)
 
 @[extern "lean_uint64_to_usize"]
-constant UInt64.toUSize (u : UInt64) : USize
+opaque UInt64.toUSize (u : UInt64) : USize
 
 @[extern "lean_usize_to_uint64"]
-constant USize.toUInt64 (u : USize) : UInt64
+opaque USize.toUInt64 (u : USize) : UInt64
 
 @[extern "lean_uint64_mix_hash"]
-constant mixHash (u₁ u₂ : UInt64) : UInt64
+opaque mixHash (u₁ u₂ : UInt64) : UInt64
 
 @[extern "lean_string_hash"]
-protected constant String.hash (s : @& String) : UInt64
+protected opaque String.hash (s : @& String) : UInt64
 
 instance : Hashable String where
   hash := String.hash
@@ -2226,7 +2226,7 @@ end Syntax
 namespace Macro
 
 /- References -/
-private constant MethodsRefPointed : NonemptyType.{0}
+private opaque MethodsRefPointed : NonemptyType.{0}
 
 private def MethodsRef : Type := MethodsRefPointed.type
 
@@ -2302,7 +2302,7 @@ unsafe def mkMethodsImp (methods : Methods) : MethodsRef :=
   unsafeCast methods
 
 @[implementedBy mkMethodsImp]
-constant mkMethods (methods : Methods) : MethodsRef
+opaque mkMethods (methods : Methods) : MethodsRef
 
 instance : Inhabited MethodsRef where
   default := mkMethods default
@@ -2310,7 +2310,7 @@ instance : Inhabited MethodsRef where
 unsafe def getMethodsImp : MacroM Methods :=
   bind read fun ctx => pure (unsafeCast (ctx.methods))
 
-@[implementedBy getMethodsImp] constant getMethods : MacroM Methods
+@[implementedBy getMethodsImp] opaque getMethods : MacroM Methods
 
 /-- `expandMacro? stx` return `some stxNew` if `stx` is a macro, and `stxNew` is its expansion. -/
 def expandMacro? (stx : Syntax) : MacroM (Option Syntax) := do

stage0/src/Init/System/IO.lean

@@ -109,17 +109,17 @@ namespace BaseIO
   to the task is dropped. The `act` should manually check for cancellation via `IO.checkCanceled` if it wants to react
   to that. -/
 @[extern "lean_io_as_task"]
-constant asTask (act : BaseIO α) (prio := Task.Priority.default) : BaseIO (Task α) :=
+opaque asTask (act : BaseIO α) (prio := Task.Priority.default) : BaseIO (Task α) :=
   Task.pure <$> act
 
 /-- See `BaseIO.asTask`. -/
 @[extern "lean_io_map_task"]
-constant mapTask (f : α → BaseIO β) (t : Task α) (prio := Task.Priority.default) : BaseIO (Task β) :=
+opaque mapTask (f : α → BaseIO β) (t : Task α) (prio := Task.Priority.default) : BaseIO (Task β) :=
   Task.pure <$> f t.get
 
 /-- See `BaseIO.asTask`. -/
 @[extern "lean_io_bind_task"]
-constant bindTask (t : Task α) (f : α → BaseIO (Task β)) (prio := Task.Priority.default) : BaseIO (Task β) :=
+opaque bindTask (t : Task α) (f : α → BaseIO (Task β)) (prio := Task.Priority.default) : BaseIO (Task β) :=
   f t.get
 
 def mapTasks (f : List α → BaseIO β) (tasks : List (Task α)) (prio := Task.Priority.default) : BaseIO (Task β) :=
@@ -163,14 +163,14 @@ def lazyPure (fn : Unit → α) : IO α :=
   pure (fn ())
 
 /-- Monotonically increasing time since an unspecified past point in milliseconds. No relation to wall clock time. -/
-@[extern "lean_io_mono_ms_now"] constant monoMsNow : BaseIO Nat
+@[extern "lean_io_mono_ms_now"] opaque monoMsNow : BaseIO Nat
 
 /-- Monotonically increasing time since an unspecified past point in nanoseconds. No relation to wall clock time. -/
-@[extern "lean_io_mono_nanos_now"] constant monoNanosNow : BaseIO Nat
+@[extern "lean_io_mono_nanos_now"] opaque monoNanosNow : BaseIO Nat
 
 /-- Read bytes from a system entropy source. Not guaranteed to be cryptographically secure.
 If `nBytes = 0`, return immediately with an empty buffer. -/
-@[extern "lean_io_get_random_bytes"] constant getRandomBytes (nBytes : USize) : IO ByteArray
+@[extern "lean_io_get_random_bytes"] opaque getRandomBytes (nBytes : USize) : IO ByteArray
 
 def sleep (ms : UInt32) : IO Unit :=
   -- TODO: add a proper primitive for IO.sleep
@@ -193,28 +193,28 @@ def sleep (ms : UInt32) : IO Unit :=
   EIO.mapTasks f tasks prio
 
 /-- Check if the task's cancellation flag has been set by calling `IO.cancel` or dropping the last reference to the task. -/
-@[extern "lean_io_check_canceled"] constant checkCanceled : BaseIO Bool
+@[extern "lean_io_check_canceled"] opaque checkCanceled : BaseIO Bool
 
 /-- Request cooperative cancellation of the task. The task must explicitly call `IO.checkCanceled` to react to the cancellation. -/
-@[extern "lean_io_cancel"] constant cancel : @& Task α → BaseIO Unit
+@[extern "lean_io_cancel"] opaque cancel : @& Task α → BaseIO Unit
 
 /-- Check if the task has finished execution, at which point calling `Task.get` will return immediately. -/
-@[extern "lean_io_has_finished"] constant hasFinished : @& Task α → BaseIO Bool
+@[extern "lean_io_has_finished"] opaque hasFinished : @& Task α → BaseIO Bool
 
 /-- Wait for the task to finish, then return its result. -/
-@[extern "lean_io_wait"] constant wait (t : Task α) : BaseIO α :=
+@[extern "lean_io_wait"] opaque wait (t : Task α) : BaseIO α :=
   return t.get
 
 /-- Wait until any of the tasks in the given list has finished, then return its result. -/
-@[extern "lean_io_wait_any"] constant waitAny : @& List (Task α) → IO α
+@[extern "lean_io_wait_any"] opaque waitAny : @& List (Task α) → IO α
 
 /-- Helper method for implementing "deterministic" timeouts. It is the number of "small" memory allocations performed by the current execution thread. -/
-@[extern "lean_io_get_num_heartbeats"] constant getNumHeartbeats : BaseIO Nat
+@[extern "lean_io_get_num_heartbeats"] opaque getNumHeartbeats : BaseIO Nat
 
 inductive FS.Mode where
   | read | write | readWrite | append
 
-constant FS.Handle : Type := Unit
+opaque FS.Handle : Type := Unit
 
 /--
   A pure-Lean abstraction of POSIX streams. We use `Stream`s for the standard streams stdin/stdout/stderr so we can
@@ -230,16 +230,16 @@ structure FS.Stream where
 
 open FS
 
-@[extern "lean_get_stdin"] constant getStdin  : BaseIO FS.Stream
-@[extern "lean_get_stdout"] constant getStdout : BaseIO FS.Stream
-@[extern "lean_get_stderr"] constant getStderr : BaseIO FS.Stream
+@[extern "lean_get_stdin"] opaque getStdin  : BaseIO FS.Stream
+@[extern "lean_get_stdout"] opaque getStdout : BaseIO FS.Stream
+@[extern "lean_get_stderr"] opaque getStderr : BaseIO FS.Stream
 
 /-- Replaces the stdin stream of the current thread and returns its previous value. -/
-@[extern "lean_get_set_stdin"] constant setStdin  : FS.Stream → BaseIO FS.Stream
+@[extern "lean_get_set_stdin"] opaque setStdin  : FS.Stream → BaseIO FS.Stream
 /-- Replaces the stdout stream of the current thread and returns its previous value. -/
-@[extern "lean_get_set_stdout"] constant setStdout : FS.Stream → BaseIO FS.Stream
+@[extern "lean_get_set_stdout"] opaque setStdout : FS.Stream → BaseIO FS.Stream
 /-- Replaces the stderr stream of the current thread and returns its previous value. -/
-@[extern "lean_get_set_stderr"] constant setStderr : FS.Stream → BaseIO FS.Stream
+@[extern "lean_get_set_stderr"] opaque setStderr : FS.Stream → BaseIO FS.Stream
 
 @[specialize] partial def iterate (a : α) (f : α → IO (Sum α β)) : IO β := do
   let v ← f a
@@ -261,7 +261,7 @@ private def fopenFlags (m : FS.Mode) (b : Bool) : String :=
   let bin := if b then "b" else "t"
   mode ++ bin
 
-@[extern "lean_io_prim_handle_mk"] constant mkPrim (fn : @& FilePath) (mode : @& String) : IO Handle
+@[extern "lean_io_prim_handle_mk"] opaque mkPrim (fn : @& FilePath) (mode : @& String) : IO Handle
 
 def mk (fn : FilePath) (Mode : Mode) (bin : Bool := true) : IO Handle :=
   mkPrim fn (fopenFlags Mode bin)
@@ -271,27 +271,27 @@ Returns whether the end of the file has been reached while reading a file.
 `h.isEof` returns true /after/ the first attempt at reading past the end of `h`.
 Once `h.isEof` is true, reading `h` will always return an empty array.
 -/
-@[extern "lean_io_prim_handle_is_eof"] constant isEof (h : @& Handle) : BaseIO Bool
-@[extern "lean_io_prim_handle_flush"] constant flush (h : @& Handle) : IO Unit
-@[extern "lean_io_prim_handle_read"] constant read  (h : @& Handle) (bytes : USize) : IO ByteArray
-@[extern "lean_io_prim_handle_write"] constant write (h : @& Handle) (buffer : @& ByteArray) : IO Unit
+@[extern "lean_io_prim_handle_is_eof"] opaque isEof (h : @& Handle) : BaseIO Bool
+@[extern "lean_io_prim_handle_flush"] opaque flush (h : @& Handle) : IO Unit
+@[extern "lean_io_prim_handle_read"] opaque read  (h : @& Handle) (bytes : USize) : IO ByteArray
+@[extern "lean_io_prim_handle_write"] opaque write (h : @& Handle) (buffer : @& ByteArray) : IO Unit
 
-@[extern "lean_io_prim_handle_get_line"] constant getLine (h : @& Handle) : IO String
-@[extern "lean_io_prim_handle_put_str"] constant putStr (h : @& Handle) (s : @& String) : IO Unit
+@[extern "lean_io_prim_handle_get_line"] opaque getLine (h : @& Handle) : IO String
+@[extern "lean_io_prim_handle_put_str"] opaque putStr (h : @& Handle) (s : @& String) : IO Unit
 
 end Handle
 
-@[extern "lean_io_realpath"] constant realPath (fname : FilePath) : IO FilePath
-@[extern "lean_io_remove_file"] constant removeFile (fname : @& FilePath) : IO Unit
+@[extern "lean_io_realpath"] opaque realPath (fname : FilePath) : IO FilePath
+@[extern "lean_io_remove_file"] opaque removeFile (fname : @& FilePath) : IO Unit
 /-- Remove given directory. Fails if not empty; see also `IO.FS.removeDirAll`. -/
-@[extern "lean_io_remove_dir"] constant removeDir : @& FilePath → IO Unit
-@[extern "lean_io_create_dir"] constant createDir : @& FilePath → IO Unit
+@[extern "lean_io_remove_dir"] opaque removeDir : @& FilePath → IO Unit
+@[extern "lean_io_create_dir"] opaque createDir : @& FilePath → IO Unit
 
 end FS
 
-@[extern "lean_io_getenv"] constant getEnv (var : @& String) : BaseIO (Option String)
-@[extern "lean_io_app_path"] constant appPath : IO FilePath
-@[extern "lean_io_current_dir"] constant currentDir : IO FilePath
+@[extern "lean_io_getenv"] opaque getEnv (var : @& String) : BaseIO (Option String)
+@[extern "lean_io_app_path"] opaque appPath : IO FilePath
+@[extern "lean_io_current_dir"] opaque currentDir : IO FilePath
 
 namespace FS
 
@@ -391,10 +391,10 @@ namespace System.FilePath
 open IO
 
 @[extern "lean_io_read_dir"]
-constant readDir : @& FilePath → IO (Array IO.FS.DirEntry)
+opaque readDir : @& FilePath → IO (Array IO.FS.DirEntry)
 
 @[extern "lean_io_metadata"]
-constant metadata : @& FilePath → IO IO.FS.Metadata
+opaque metadata : @& FilePath → IO IO.FS.Metadata
 
 def isDir (p : FilePath) : BaseIO Bool := do
   match (← p.metadata.toBaseIO) with
@@ -534,9 +534,9 @@ structure Child (cfg : StdioConfig) where
   stdout : cfg.stdout.toHandleType
   stderr : cfg.stderr.toHandleType
 
-@[extern "lean_io_process_spawn"] constant spawn (args : SpawnArgs) : IO (Child args.toStdioConfig)
+@[extern "lean_io_process_spawn"] opaque spawn (args : SpawnArgs) : IO (Child args.toStdioConfig)
 
-@[extern "lean_io_process_child_wait"] constant Child.wait {cfg : @& StdioConfig} : @& Child cfg → IO UInt32
+@[extern "lean_io_process_child_wait"] opaque Child.wait {cfg : @& StdioConfig} : @& Child cfg → IO UInt32
 
 /--
 Extract the `stdin` field from a `Child` object, allowing them to be freed independently.
@@ -544,7 +544,7 @@ This operation is necessary for closing the child process' stdin while still hol
 e.g. for `Child.wait`. A file handle is closed when all references to it are dropped, which without this
 operation includes the `Child` object.
 -/
-@[extern "lean_io_process_child_take_stdin"] constant Child.takeStdin {cfg : @& StdioConfig} : Child cfg →
+@[extern "lean_io_process_child_take_stdin"] opaque Child.takeStdin {cfg : @& StdioConfig} : Child cfg →
     IO (cfg.stdin.toHandleType × Child { cfg with stdin := Stdio.null })
 
 structure Output where
@@ -568,7 +568,7 @@ def run (args : SpawnArgs) : IO String := do
     throw <| IO.userError <| "process '" ++ args.cmd ++ "' exited with code " ++ toString out.exitCode
   pure out.stdout
 
-@[extern "lean_io_exit"] constant exit : UInt8 → IO α
+@[extern "lean_io_exit"] opaque exit : UInt8 → IO α
 
 end Process
 
@@ -594,7 +594,7 @@ def FileRight.flags (acc : FileRight) : UInt32 :=
   let o : UInt32 := acc.other.flags
   u.lor <| g.lor o
 
-@[extern "lean_chmod"] constant Prim.setAccessRights (filename : @& FilePath) (mode : UInt32) : IO Unit
+@[extern "lean_chmod"] opaque Prim.setAccessRights (filename : @& FilePath) (mode : UInt32) : IO Unit
 
 def setAccessRights (filename : FilePath) (mode : FileRight) : IO Unit :=
   Prim.setAccessRights filename mode.flags

stage0/src/Init/System/ST.lean

@@ -42,7 +42,7 @@ instance {ε σ} : MonadLift (ST σ) (EST ε σ) := ⟨fun x s =>
 namespace ST
 
 /- References -/
-constant RefPointed : NonemptyType.{0}
+opaque RefPointed : NonemptyType.{0}
 
 structure Ref (σ : Type) (α : Type) : Type where
   ref : RefPointed.type
@@ -59,17 +59,17 @@ private noncomputable def inhabitedFromRef {σ α} (r : Ref σ α) : ST σ α :=
   pure default
 
 @[extern "lean_st_mk_ref"]
-constant mkRef {σ α} (a : α) : ST σ (Ref σ α) := pure { ref := Classical.choice RefPointed.property, h := Nonempty.intro a }
+opaque mkRef {σ α} (a : α) : ST σ (Ref σ α) := pure { ref := Classical.choice RefPointed.property, h := Nonempty.intro a }
 @[extern "lean_st_ref_get"]
-constant Ref.get {σ α} (r : @& Ref σ α) : ST σ α := inhabitedFromRef r
+opaque Ref.get {σ α} (r : @& Ref σ α) : ST σ α := inhabitedFromRef r
 @[extern "lean_st_ref_set"]
-constant Ref.set {σ α} (r : @& Ref σ α) (a : α) : ST σ Unit
+opaque Ref.set {σ α} (r : @& Ref σ α) (a : α) : ST σ Unit
 @[extern "lean_st_ref_swap"]
-constant Ref.swap {σ α} (r : @& Ref σ α) (a : α) : ST σ α := inhabitedFromRef r
+opaque Ref.swap {σ α} (r : @& Ref σ α) (a : α) : ST σ α := inhabitedFromRef r
 @[extern "lean_st_ref_take"]
-unsafe constant Ref.take {σ α} (r : @& Ref σ α) : ST σ α := inhabitedFromRef r
+unsafe opaque Ref.take {σ α} (r : @& Ref σ α) : ST σ α := inhabitedFromRef r
 @[extern "lean_st_ref_ptr_eq"]
-constant Ref.ptrEq {σ α} (r1 r2 : @& Ref σ α) : ST σ Bool
+opaque Ref.ptrEq {σ α} (r1 r2 : @& Ref σ α) : ST σ Bool
 
 @[inline] unsafe def Ref.modifyUnsafe {σ α : Type} (r : Ref σ α) (f : α → α) : ST σ Unit := do
   let v ← Ref.take r

stage0/src/Lean/Attributes.lean

@@ -327,7 +327,7 @@ unsafe def mkAttributeImplOfConstantUnsafe (env : Environment) (opts : Options)
     | _ => throw ("unexpected attribute implementation type at '" ++ toString declName ++ "' (`AttributeImpl` expected")
 
 @[implementedBy mkAttributeImplOfConstantUnsafe]
-constant mkAttributeImplOfConstant (env : Environment) (opts : Options) (declName : Name) : Except String AttributeImpl
+opaque mkAttributeImplOfConstant (env : Environment) (opts : Options) (declName : Name) : Except String AttributeImpl
 
 def mkAttributeImplOfEntry (env : Environment) (opts : Options) (e : AttributeExtensionOLeanEntry) : IO AttributeImpl :=
   match e with

stage0/src/Lean/Compiler/ExternAttr.lean

@@ -56,7 +56,7 @@ private def syntaxToExternAttrData (stx : Syntax) : AttrM ExternAttrData := do
   return { arity? := arity?, entries := entries.toList }
 
 @[extern "lean_add_extern"]
-constant addExtern (env : Environment) (n : Name) : ExceptT String Id Environment
+opaque addExtern (env : Environment) (n : Name) : ExceptT String Id Environment
 
 builtin_initialize externAttr : ParametricAttribute ExternAttrData ←
   registerParametricAttribute {

stage0/src/Lean/Compiler/IR/Checker.lean

@@ -9,15 +9,15 @@ import Lean.Compiler.IR.Format
 namespace Lean.IR.Checker
 
 @[extern c inline "lean_box(LEAN_MAX_CTOR_FIELDS)"]
-constant getMaxCtorFields : Unit → Nat
+opaque getMaxCtorFields : Unit → Nat
 def maxCtorFields := getMaxCtorFields ()
 
 @[extern c inline "lean_box(LEAN_MAX_CTOR_SCALARS_SIZE)"]
-constant getMaxCtorScalarsSize : Unit → Nat
+opaque getMaxCtorScalarsSize : Unit → Nat
 def maxCtorScalarsSize := getMaxCtorScalarsSize ()
 
 @[extern c inline "lean_box(sizeof(size_t))"]
-constant getUSizeSize : Unit → Nat
+opaque getUSizeSize : Unit → Nat
 def usizeSize := getUSizeSize ()
 
 structure CheckerContext where

stage0/src/Lean/Compiler/IR/CtorLayout.lean

@@ -35,7 +35,7 @@ structure CtorLayout where
   scalarSize : Nat
 
 @[extern "lean_ir_get_ctor_layout"]
-constant getCtorLayout (env : @& Environment) (ctorName : @& Name) : Except String CtorLayout
+opaque getCtorLayout (env : @& Environment) (ctorName : @& Name) : Except String CtorLayout
 
 end IR
 end Lean

stage0/src/Lean/Compiler/InitAttr.lean

@@ -70,7 +70,7 @@ unsafe def registerInitAttrUnsafe (attrName : Name) (runAfterImport : Bool) : IO
   }
 
 @[implementedBy registerInitAttrUnsafe]
-constant registerInitAttr (attrName : Name) (runAfterImport : Bool) : IO (ParametricAttribute Name)
+opaque registerInitAttr (attrName : Name) (runAfterImport : Bool) : IO (ParametricAttribute Name)
 
 builtin_initialize regularInitAttr : ParametricAttribute Name ← registerInitAttr `init true
 builtin_initialize builtinInitAttr : ParametricAttribute Name ← registerInitAttr `builtinInit false

stage0/src/Lean/Declaration.lean

@@ -403,10 +403,10 @@ def isInductive : ConstantInfo → Bool
   | _            => false
 
 @[extern "lean_instantiate_type_lparams"]
-constant instantiateTypeLevelParams (c : @& ConstantInfo) (ls : @& List Level) : Expr
+opaque instantiateTypeLevelParams (c : @& ConstantInfo) (ls : @& List Level) : Expr
 
 @[extern "lean_instantiate_value_lparams"]
-constant instantiateValueLevelParams (c : @& ConstantInfo) (ls : @& List Level) : Expr
+opaque instantiateValueLevelParams (c : @& ConstantInfo) (ls : @& List Level) : Expr
 
 end ConstantInfo
 

stage0/src/Lean/Elab/BuiltinCommand.lean

@@ -355,7 +355,7 @@ unsafe def elabEvalUnsafe : CommandElab
   | _ => throwUnsupportedSyntax
 
 @[builtinCommandElab «eval», implementedBy elabEvalUnsafe]
-constant elabEval : CommandElab
+opaque elabEval : CommandElab
 
 @[builtinCommandElab «synth»] def elabSynth : CommandElab := fun stx => do
   let term := stx[1]

stage0/src/Lean/Elab/Command.lean

@@ -218,7 +218,7 @@ unsafe def mkCommandElabAttributeUnsafe : IO (KeyedDeclsAttribute CommandElab) :
   mkElabAttribute CommandElab `Lean.Elab.Command.commandElabAttribute `builtinCommandElab `commandElab `Lean.Parser.Command `Lean.Elab.Command.CommandElab "command"
 
 @[implementedBy mkCommandElabAttributeUnsafe]
-constant mkCommandElabAttribute : IO (KeyedDeclsAttribute CommandElab)
+opaque mkCommandElabAttribute : IO (KeyedDeclsAttribute CommandElab)
 
 builtin_initialize commandElabAttribute : KeyedDeclsAttribute CommandElab ← mkCommandElabAttribute
 

stage0/src/Lean/Elab/Declaration.lean

@@ -57,7 +57,6 @@ private def expandDeclNamespace? (stx : Syntax) : MacroM (Option (Name × Syntax
     if k == ``Lean.Parser.Command.abbrev ||
        k == ``Lean.Parser.Command.def ||
        k == ``Lean.Parser.Command.theorem ||
-       k == ``Lean.Parser.Command.constant || -- TODO: delete
        k == ``Lean.Parser.Command.opaque ||
        k == ``Lean.Parser.Command.axiom ||
        k == ``Lean.Parser.Command.inductive ||
@@ -326,13 +325,13 @@ def expandInitCmd (builtin : Bool) : Macro := fun stx => do
     let type := optHeader[1][1]
     if optVisibility.isNone then
       `(def initFn : IO $type := do $doSeq
-        @[$attrId:ident initFn] constant $id : $type)
+        @[$attrId:ident initFn] opaque $id : $type)
     else if optVisibility[0].getKind == ``Parser.Command.private then
       `(def initFn : IO $type := do $doSeq
-        @[$attrId:ident initFn] private constant $id : $type)
+        @[$attrId:ident initFn] private opaque $id : $type)
     else if optVisibility[0].getKind == ``Parser.Command.protected then
       `(def initFn : IO $type := do $doSeq
-        @[$attrId:ident initFn] protected constant $id : $type)
+        @[$attrId:ident initFn] protected opaque $id : $type)
     else
       Macro.throwError "unexpected visibility annotation"
 

stage0/src/Lean/Elab/DefView.lean

@@ -147,7 +147,6 @@ def isDefLike (stx : Syntax) : Bool :=
   declKind == ``Parser.Command.abbrev ||
   declKind == ``Parser.Command.def ||
   declKind == ``Parser.Command.theorem ||
-  declKind == ``Parser.Command.constant || -- TODO: delete
   declKind == ``Parser.Command.opaque ||
   declKind == ``Parser.Command.instance ||
   declKind == ``Parser.Command.example
@@ -160,8 +159,6 @@ def mkDefView (modifiers : Modifiers) (stx : Syntax) : CommandElabM DefView :=
     return mkDefViewOfDef modifiers stx
   else if declKind == ``Parser.Command.theorem then
     return mkDefViewOfTheorem modifiers stx
-  else if declKind == ``Parser.Command.constant then -- TODO: delete
-    mkDefViewOfOpaque modifiers stx
   else if declKind == ``Parser.Command.opaque then
     mkDefViewOfOpaque modifiers stx
   else if declKind == ``Parser.Command.instance then

stage0/src/Lean/Elab/MutualDef.lean

@@ -79,7 +79,7 @@ private def registerFailedToInferDefTypeInfo (type : Expr) (ref : Syntax) : Term
 /--
   Return `some [b, c]` if the given `views` are representing a declaration of the form
   ```
-  constant a b c : Nat
+  opaque a b c : Nat
   ```  -/
 private def isMultiConstant? (views : Array DefView) : Option (List Name) :=
   if views.size == 1 &&

stage0/src/Lean/Elab/Print.lean

@@ -68,7 +68,7 @@ private def printIdCore (id : Name) : CommandElabM Unit := do
   | ConstantInfo.axiomInfo { levelParams := us, type := t, isUnsafe := u, .. } => printAxiomLike "axiom" id us t u
   | ConstantInfo.defnInfo  { levelParams := us, type := t, value := v, safety := s, .. } => printDefLike "def" id us t v s
   | ConstantInfo.thmInfo  { levelParams := us, type := t, value := v, .. } => printDefLike "theorem" id us t v
-  | ConstantInfo.opaqueInfo  { levelParams := us, type := t, isUnsafe := u, .. } => printAxiomLike "constant" id us t u
+  | ConstantInfo.opaqueInfo  { levelParams := us, type := t, isUnsafe := u, .. } => printAxiomLike "opaque" id us t u
   | ConstantInfo.quotInfo  { levelParams := us, type := t, .. } => printQuot id us t
   | ConstantInfo.ctorInfo { levelParams := us, type := t, isUnsafe := u, .. } => printAxiomLike "constructor" id us t u
   | ConstantInfo.recInfo { levelParams := us, type := t, isUnsafe := u, .. } => printAxiomLike "recursor" id us t u

stage0/src/Lean/Elab/Structure.lean

@@ -688,7 +688,7 @@ private def mkCtor (view : StructView) (levelParams : List Name) (params : Array
   pure { name := view.ctor.declName, type }
 
 @[extern "lean_mk_projections"]
-private constant mkProjections (env : Environment) (structName : Name) (projs : List Name) (isClass : Bool) : Except KernelException Environment
+private opaque mkProjections (env : Environment) (structName : Name) (projs : List Name) (isClass : Bool) : Except KernelException Environment
 
 private def addProjections (structName : Name) (projs : List Name) (isClass : Bool) : TermElabM Unit := do
   let env ← getEnv

stage0/src/Lean/Elab/Term.lean

@@ -320,7 +320,7 @@ unsafe def mkTermElabAttributeUnsafe : IO (KeyedDeclsAttribute TermElab) :=
   mkElabAttribute TermElab `Lean.Elab.Term.termElabAttribute `builtinTermElab `termElab `Lean.Parser.Term `Lean.Elab.Term.TermElab "term"
 
 @[implementedBy mkTermElabAttributeUnsafe]
-constant mkTermElabAttribute : IO (KeyedDeclsAttribute TermElab)
+opaque mkTermElabAttribute : IO (KeyedDeclsAttribute TermElab)
 
 builtin_initialize termElabAttribute : KeyedDeclsAttribute TermElab ← mkTermElabAttribute
 

stage0/src/Lean/Elab/Util.lean

@@ -95,7 +95,7 @@ private unsafe def evalSyntaxConstantUnsafe (env : Environment) (opts : Options)
   env.evalConstCheck Syntax opts `Lean.Syntax constName
 
 @[implementedBy evalSyntaxConstantUnsafe]
-constant evalSyntaxConstant (env : Environment) (opts : Options) (constName : Name) : ExceptT String Id Syntax := throw ""
+opaque evalSyntaxConstant (env : Environment) (opts : Options) (constName : Name) : ExceptT String Id Syntax := throw ""
 
 unsafe def mkElabAttribute (γ) (attrDeclName attrBuiltinName attrName : Name) (parserNamespace : Name) (typeName : Name) (kind : String)
     : IO (KeyedDeclsAttribute γ) :=
@@ -117,7 +117,7 @@ unsafe def mkMacroAttributeUnsafe : IO (KeyedDeclsAttribute Macro) :=
   mkElabAttribute Macro `Lean.Elab.macroAttribute `builtinMacro `macro Name.anonymous `Lean.Macro "macro"
 
 @[implementedBy mkMacroAttributeUnsafe]
-constant mkMacroAttribute : IO (KeyedDeclsAttribute Macro)
+opaque mkMacroAttribute : IO (KeyedDeclsAttribute Macro)
 
 builtin_initialize macroAttribute : KeyedDeclsAttribute Macro ← mkMacroAttribute
 

stage0/src/Lean/Environment.lean

@@ -14,7 +14,7 @@ import Lean.Util.Profile
 
 namespace Lean
 /- Opaque environment extension state. -/
-constant EnvExtensionStateSpec : (α : Type) × Inhabited α := ⟨Unit, ⟨()⟩⟩
+opaque EnvExtensionStateSpec : (α : Type) × Inhabited α := ⟨Unit, ⟨()⟩⟩
 def EnvExtensionState : Type := EnvExtensionStateSpec.fst
 instance : Inhabited EnvExtensionState := EnvExtensionStateSpec.snd
 
@@ -37,14 +37,14 @@ instance : ToString Import := ⟨fun imp => toString imp.module ++ if imp.runtim
 def CompactedRegion := USize
 
 @[extern "lean_compacted_region_is_memory_mapped"]
-constant CompactedRegion.isMemoryMapped : CompactedRegion → Bool
+opaque CompactedRegion.isMemoryMapped : CompactedRegion → Bool
 
 /-- Free a compacted region and its contents. No live references to the contents may exist at the time of invocation. -/
 @[extern "lean_compacted_region_free"]
-unsafe constant CompactedRegion.free : CompactedRegion → IO Unit
+unsafe opaque CompactedRegion.free : CompactedRegion → IO Unit
 
 /- Opaque persistent environment extension entry. -/
-constant EnvExtensionEntrySpec : NonemptyType.{0}
+opaque EnvExtensionEntrySpec : NonemptyType.{0}
 def EnvExtensionEntry : Type := EnvExtensionEntrySpec.type
 instance : Nonempty EnvExtensionEntry := EnvExtensionEntrySpec.property
 
@@ -146,11 +146,11 @@ namespace Environment
 
 /- Type check given declaration and add it to the environment -/
 @[extern "lean_add_decl"]
-constant addDecl (env : Environment) (decl : @& Declaration) : Except KernelException Environment
+opaque addDecl (env : Environment) (decl : @& Declaration) : Except KernelException Environment
 
 /- Compile the given declaration, it assumes the declaration has already been added to the environment using `addDecl`. -/
 @[extern "lean_compile_decl"]
-constant compileDecl (env : Environment) (opt : @& Options) (decl : @& Declaration) : Except KernelException Environment
+opaque compileDecl (env : Environment) (opt : @& Options) (decl : @& Declaration) : Except KernelException Environment
 
 def addAndCompile (env : Environment) (opt : Options) (decl : Declaration) : Except KernelException Environment := do
   let env ← addDecl env decl
@@ -265,7 +265,7 @@ unsafe def imp : EnvExtensionInterface := {
 end EnvExtensionInterfaceUnsafe
 
 @[implementedBy EnvExtensionInterfaceUnsafe.imp]
-constant EnvExtensionInterfaceImp : EnvExtensionInterface
+opaque EnvExtensionInterfaceImp : EnvExtensionInterface
 
 def EnvExtension (σ : Type) : Type := EnvExtensionInterfaceImp.ext σ
 
@@ -401,7 +401,7 @@ unsafe def registerPersistentEnvExtensionUnsafe {α β σ : Type} [Inhabited σ]
   return pExt
 
 @[implementedBy registerPersistentEnvExtensionUnsafe]
-constant registerPersistentEnvExtension {α β σ : Type} [Inhabited σ] (descr : PersistentEnvExtensionDescr α β σ) : IO (PersistentEnvExtension α β σ)
+opaque registerPersistentEnvExtension {α β σ : Type} [Inhabited σ] (descr : PersistentEnvExtensionDescr α β σ) : IO (PersistentEnvExtension α β σ)
 
 /- Simple PersistentEnvExtension that implements exportEntriesFn using a list of entries. -/
 
@@ -512,9 +512,9 @@ def contains [Inhabited α] (ext : MapDeclarationExtension α) (env : Environmen
 end MapDeclarationExtension
 
 @[extern "lean_save_module_data"]
-constant saveModuleData (fname : @& System.FilePath) (mod : @& Name) (data : @& ModuleData) : IO Unit
+opaque saveModuleData (fname : @& System.FilePath) (mod : @& Name) (data : @& ModuleData) : IO Unit
 @[extern "lean_read_module_data"]
-constant readModuleData (fname : @& System.FilePath) : IO (ModuleData × CompactedRegion)
+opaque readModuleData (fname : @& System.FilePath) : IO (ModuleData × CompactedRegion)
 
 /--
   Free compacted regions of imports. No live references to imported objects may exist at the time of invocation; in
@@ -582,9 +582,9 @@ private def setImportedEntries (env : Environment) (mods : Array ModuleData) (st
   When we a new user-defined attribute declaration is imported, `attributeMapRef` is updated.
   Later, we set this method with code that adds the user-defined attributes that were imported after we initialized `attributeExtension`.
 -/
-@[extern 2 "lean_update_env_attributes"] constant updateEnvAttributes : Environment → IO Environment
+@[extern 2 "lean_update_env_attributes"] opaque updateEnvAttributes : Environment → IO Environment
 /-- "Forward declaration" for retrieving the number of builtin attributes. -/
-@[extern 1 "lean_get_num_attributes"] constant getNumBuiltiAttributes : IO Nat
+@[extern 1 "lean_get_num_attributes"] opaque getNumBuiltiAttributes : IO Nat
 
 private partial def finalizePersistentExtensions (env : Environment) (mods : Array ModuleData) (opts : Options) : IO Environment := do
   loop 0 env
@@ -736,7 +736,7 @@ def displayStats (env : Environment) : IO Unit := do
   This function is only safe to use if the type matches the declaration's type in the environment
   and if `enableInitializersExecution` has been used before importing any modules. -/
 @[extern "lean_eval_const"]
-unsafe constant evalConst (α) (env : @& Environment) (opts : @& Options) (constName : @& Name) : Except String α
+unsafe opaque evalConst (α) (env : @& Environment) (opts : @& Options) (constName : @& Name) : Except String α
 
 private def throwUnexpectedType {α} (typeName : Name) (constName : Name) : ExceptT String Id α :=
   throw ("unexpected type at '" ++ toString constName ++ "', `" ++ toString typeName ++ "` expected")
@@ -772,14 +772,14 @@ namespace Kernel
   Recall that the Kernel type checker does not support metavariables.
   When implementing automation, consider using the `MetaM` methods. -/
 @[extern "lean_kernel_is_def_eq"]
-constant isDefEq (env : Environment) (lctx : LocalContext) (a b : Expr) : Bool
+opaque isDefEq (env : Environment) (lctx : LocalContext) (a b : Expr) : Bool
 
 /--
   Kernel WHNF function. We use it mainly for debugging purposes.
   Recall that the Kernel type checker does not support metavariables.
   When implementing automation, consider using the `MetaM` methods. -/
 @[extern "lean_kernel_whnf"]
-constant whnf (env : Environment) (lctx : LocalContext) (a : Expr) : Expr
+opaque whnf (env : Environment) (lctx : LocalContext) (a : Expr) : Expr
 
 end Kernel
 

stage0/src/Lean/Expr.lean

@@ -461,18 +461,18 @@ def mkAppRev (fn : Expr) (revArgs : Array Expr) : Expr :=
 namespace Expr
 -- TODO: implement it in Lean
 @[extern "lean_expr_dbg_to_string"]
-constant dbgToString (e : @& Expr) : String
+opaque dbgToString (e : @& Expr) : String
 
 @[extern "lean_expr_quick_lt"]
-constant quickLt (a : @& Expr) (b : @& Expr) : Bool
+opaque quickLt (a : @& Expr) (b : @& Expr) : Bool
 
 @[extern "lean_expr_lt"]
-constant lt (a : @& Expr) (b : @& Expr) : Bool
+opaque lt (a : @& Expr) (b : @& Expr) : Bool
 
 /-- Return true iff `a` and `b` are alpha equivalent.
    Binder annotations are ignored. -/
 @[extern "lean_expr_eqv"]
-constant eqv (a : @& Expr) (b : @& Expr) : Bool
+opaque eqv (a : @& Expr) (b : @& Expr) : Bool
 
 instance : BEq Expr where
   beq := Expr.eqv
@@ -483,7 +483,7 @@ protected unsafe def ptrEq (a b : Expr) : Bool :=
 /- Return true iff `a` and `b` are equal.
    Binder names and annotations are taking into account. -/
 @[extern "lean_expr_equal"]
-constant equal (a : @& Expr) (b : @& Expr) : Bool
+opaque equal (a : @& Expr) (b : @& Expr) : Bool
 
 def isSort : Expr → Bool
   | sort .. => true
@@ -770,7 +770,7 @@ def isArrow (e : Expr) : Bool :=
   | _ => false
 
 @[extern "lean_expr_has_loose_bvar"]
-constant hasLooseBVar (e : @& Expr) (bvarIdx : @& Nat) : Bool
+opaque hasLooseBVar (e : @& Expr) (bvarIdx : @& Nat) : Bool
 
 /-- Return true if `e` contains the loose bound variable `bvarIdx` in an explicit parameter, or in the range if `tryRange == true`. -/
 def hasLooseBVarInExplicitDomain : Expr → Nat → Bool → Bool
@@ -784,12 +784,12 @@ def hasLooseBVarInExplicitDomain : Expr → Nat → Bool → Bool
 
   Remark: if `s < d`, then result is `e` -/
 @[extern "lean_expr_lower_loose_bvars"]
-constant lowerLooseBVars (e : @& Expr) (s d : @& Nat) : Expr
+opaque lowerLooseBVars (e : @& Expr) (s d : @& Nat) : Expr
 
 /--
   Lift loose bound variables `>= s` in `e` by `d`. -/
 @[extern "lean_expr_lift_loose_bvars"]
-constant liftLooseBVars (e : @& Expr) (s d : @& Nat) : Expr
+opaque liftLooseBVars (e : @& Expr) (s d : @& Nat) : Expr
 
 /--
   `inferImplicit e numParams considerRange` updates the first `numParams` parameter binder annotations of the `e` forall type.
@@ -810,32 +810,32 @@ def inferImplicit : Expr → Nat → Bool → Expr
 /-- Instantiate the loose bound variables in `e` using `subst`.
     That is, a loose `Expr.bvar i` is replaced with `subst[i]`. -/
 @[extern "lean_expr_instantiate"]
-constant instantiate (e : @& Expr) (subst : @& Array Expr) : Expr
+opaque instantiate (e : @& Expr) (subst : @& Array Expr) : Expr
 
 @[extern "lean_expr_instantiate1"]
-constant instantiate1 (e : @& Expr) (subst : @& Expr) : Expr
+opaque instantiate1 (e : @& Expr) (subst : @& Expr) : Expr
 
 /-- Similar to instantiate, but `Expr.bvar i` is replaced with `subst[subst.size - i - 1]` -/
 @[extern "lean_expr_instantiate_rev"]
-constant instantiateRev (e : @& Expr) (subst : @& Array Expr) : Expr
+opaque instantiateRev (e : @& Expr) (subst : @& Array Expr) : Expr
 
 /-- Similar to `instantiate`, but consider only the variables `xs` in the range `[beginIdx, endIdx)`.
     Function panics if `beginIdx <= endIdx <= xs.size` does not hold. -/
 @[extern "lean_expr_instantiate_range"]
-constant instantiateRange (e : @& Expr) (beginIdx endIdx : @& Nat) (xs : @& Array Expr) : Expr
+opaque instantiateRange (e : @& Expr) (beginIdx endIdx : @& Nat) (xs : @& Array Expr) : Expr
 
 /-- Similar to `instantiateRev`, but consider only the variables `xs` in the range `[beginIdx, endIdx)`.
     Function panics if `beginIdx <= endIdx <= xs.size` does not hold. -/
 @[extern "lean_expr_instantiate_rev_range"]
-constant instantiateRevRange (e : @& Expr) (beginIdx endIdx : @& Nat) (xs : @& Array Expr) : Expr
+opaque instantiateRevRange (e : @& Expr) (beginIdx endIdx : @& Nat) (xs : @& Array Expr) : Expr
 
 /-- Replace free (or meta) variables `xs` with loose bound variables. -/
 @[extern "lean_expr_abstract"]
-constant abstract (e : @& Expr) (xs : @& Array Expr) : Expr
+opaque abstract (e : @& Expr) (xs : @& Array Expr) : Expr
 
 /-- Similar to `abstract`, but consider only the first `min n xs.size` entries in `xs`. -/
 @[extern "lean_expr_abstract_range"]
-constant abstractRange (e : @& Expr) (n : @& Nat) (xs : @& Array Expr) : Expr
+opaque abstractRange (e : @& Expr) (n : @& Nat) (xs : @& Array Expr) : Expr
 
 /-- Replace occurrences of the free variable `fvar` in `e` with `v` -/
 def replaceFVar (e : Expr) (fvar : Expr) (v : Expr) : Expr :=

stage0/src/Lean/Linter/Basic.lean

@@ -152,7 +152,7 @@ where
   isInConstantOrAxiom (_ : Syntax) (stack : SyntaxStack) :=
     stackMatches stack [`null, none, `null, ``Lean.Parser.Command.declSig, none] &&
     (stack.get? 4 |>.any fun (stx, _) =>
-      [``Lean.Parser.Command.constant, ``Lean.Parser.Command.axiom].any (stx.isOfKind ·))
+      [``Lean.Parser.Command.opaque, ``Lean.Parser.Command.axiom].any (stx.isOfKind ·))
   isInDefWithForeignDefinition (_ : Syntax) (stack : SyntaxStack) :=
     stackMatches stack [`null, none, `null, none, none, ``Lean.Parser.Command.declaration] &&
     (stack.get? 3 |>.any fun (stx, _) =>

stage0/src/Lean/LoadDynlib.lean

@@ -14,4 +14,4 @@ Equivalent to passing `--load-dynlib=lib` to `lean`.
 Note that Lean never unloads libraries.
 -/
 @[extern "lean_load_dynlib"]
-constant loadDynlib (path : @& System.FilePath) : IO Unit
+opaque loadDynlib (path : @& System.FilePath) : IO Unit

stage0/src/Lean/Meta/ACLt.lean

@@ -155,6 +155,6 @@ end
 end ACLt
 
 @[implementedBy ACLt.lt]
-constant Expr.acLt : Expr → Expr → MetaM Bool
+opaque Expr.acLt : Expr → Expr → MetaM Bool
 
 end Lean.Meta

stage0/src/Lean/Meta/Match/MatchEqsExt.lean

@@ -31,6 +31,6 @@ def registerMatchEqns (matchDeclName : Name) (matchEqns : MatchEqns) : CoreM Uni
   Forward definition. We want to use `getEquationsFor` in the simplifier,
  `getEquationsFor` depends on `mkEquationsfor` which uses the simplifier. -/
 @[extern "lean_get_match_equations_for"]
-constant getEquationsFor (matchDeclName : Name) : MetaM MatchEqns
+opaque getEquationsFor (matchDeclName : Name) : MetaM MatchEqns
 
 end Lean.Meta.Match

stage0/src/Lean/Meta/WHNF.lean

@@ -25,7 +25,7 @@ It is possible to avoid this hack if we move `Structural.EqnInfo` and `Structura
 to this module.
 -/
 @[extern "lean_get_structural_rec_arg_pos"]
-constant getStructuralRecArgPos? (declName : Name) : CoreM (Option Nat)
+opaque getStructuralRecArgPos? (declName : Name) : CoreM (Option Nat)
 
 def smartUnfoldingSuffix := "_sunfold"
 
@@ -720,8 +720,8 @@ def reduceRecMatcher? (e : Expr) : MetaM (Option Expr) := do
 
 unsafe def reduceBoolNativeUnsafe (constName : Name) : MetaM Bool := evalConstCheck Bool `Bool constName
 unsafe def reduceNatNativeUnsafe (constName : Name) : MetaM Nat := evalConstCheck Nat `Nat constName
-@[implementedBy reduceBoolNativeUnsafe] constant reduceBoolNative (constName : Name) : MetaM Bool
-@[implementedBy reduceNatNativeUnsafe] constant reduceNatNative (constName : Name) : MetaM Nat
+@[implementedBy reduceBoolNativeUnsafe] opaque reduceBoolNative (constName : Name) : MetaM Bool
+@[implementedBy reduceNatNativeUnsafe] opaque reduceNatNative (constName : Name) : MetaM Nat
 
 def reduceNative? (e : Expr) : MetaM (Option Expr) :=
   match e with

stage0/src/Lean/Parser/Command.lean

@@ -70,7 +70,6 @@ def «abbrev»         := leading_parser "abbrev " >> declId >> ppIndent optDecl
 def optDefDeriving   := optional (atomic ("deriving " >> notSymbol "instance") >> sepBy1 ident ", ")
 def «def»            := leading_parser "def " >> declId >> ppIndent optDeclSig >> declVal >> optDefDeriving >> terminationSuffix
 def «theorem»        := leading_parser "theorem " >> declId >> ppIndent declSig >> declVal >> terminationSuffix
-def «constant»       := leading_parser "constant " >> declId >> ppIndent declSig >> optional declValSimple
 def «opaque»         := leading_parser "opaque " >> declId >> ppIndent declSig >> optional declValSimple
 /- As `declSig` starts with a space, "instance" does not need a trailing space if we put `ppSpace` in the optional fragments. -/
 def «instance»       := leading_parser Term.attrKind >> "instance" >> optNamedPrio >> optional (ppSpace >> declId) >> ppIndent declSig >> declVal >> terminationSuffix
@@ -96,7 +95,7 @@ def «structure»          := leading_parser
     >> optional ((symbol " := " <|> " where ") >> optional structCtor >> structFields)
     >> optDeriving
 @[builtinCommandParser] def declaration := leading_parser
-declModifiers false >> («abbrev» <|> «def» <|> «theorem» <|> «constant» <|> «opaque» <|> «instance» <|> «axiom» <|> «example» <|> «inductive» <|> classInductive <|> «structure»)
+declModifiers false >> («abbrev» <|> «def» <|> «theorem» <|> «opaque» <|> «instance» <|> «axiom» <|> «example» <|> «inductive» <|> classInductive <|> «structure»)
 @[builtinCommandParser] def «deriving»     := leading_parser "deriving " >> "instance " >> derivingClasses >> " for " >> sepBy1 ident ", "
 @[builtinCommandParser] def noncomputableSection := leading_parser "noncomputable " >> "section " >> optional ident
 @[builtinCommandParser] def «section»      := leading_parser "section " >> optional ident

stage0/src/Lean/Parser/Extension.lean

@@ -250,7 +250,7 @@ unsafe def mkParserOfConstantUnsafe (constName : Name) (compileParserDescr : Par
     | _ => throw ↑s!"unexpected parser type at '{constName}' (`ParserDescr`, `TrailingParserDescr`, `Parser` or `TrailingParser` expected)"
 
 @[implementedBy mkParserOfConstantUnsafe]
-constant mkParserOfConstantAux (constName : Name) (compileParserDescr : ParserDescr → ImportM Parser) : ImportM (Bool × Parser)
+opaque mkParserOfConstantAux (constName : Name) (compileParserDescr : ParserDescr → ImportM Parser) : ImportM (Bool × Parser)
 
 partial def compileParserDescr (categories : ParserCategories) (d : ParserDescr) : ImportM Parser :=
   let rec visit : ParserDescr → ImportM Parser
@@ -345,7 +345,7 @@ unsafe def evalParserConstUnsafe (declName : Name) : ParserFn := fun ctx s => un
   | .error e   => return s.mkUnexpectedError e.toString
 
 @[implementedBy evalParserConstUnsafe]
-constant evalParserConst (declName : Name) : ParserFn
+opaque evalParserConst (declName : Name) : ParserFn
 
 register_builtin_option internal.parseQuotWithCurrentStage : Bool := {
   defValue := false

stage0/src/Lean/PrettyPrinter/Formatter.lean

@@ -177,11 +177,11 @@ def withMaybeTag (pos? : Option String.Pos) (x : FormatterM Unit) : Formatter :=
 -- `categoryParser -> mkAntiquot -> termParser -> categoryParser`, so we need to introduce an indirection somewhere
 -- anyway.
 @[extern "lean_mk_antiquot_formatter"]
-constant mkAntiquot.formatter' (name : String) (kind : Option SyntaxNodeKind) (anonymous := true) : Formatter
+opaque mkAntiquot.formatter' (name : String) (kind : Option SyntaxNodeKind) (anonymous := true) : Formatter
 
 -- break up big mutual recursion
 @[extern "lean_pretty_printer_formatter_interpret_parser_descr"]
-constant interpretParserDescr' : ParserDescr → CoreM Formatter
+opaque interpretParserDescr' : ParserDescr → CoreM Formatter
 
 private def SourceInfo.getExprPos? : SourceInfo → Option String.Pos
   | SourceInfo.synthetic pos _ => pos
@@ -203,7 +203,7 @@ unsafe def formatterForKindUnsafe (k : SyntaxNodeKind) : Formatter := do
     withMaybeTag (getExprPos? stx) f
 
 @[implementedBy formatterForKindUnsafe]
-constant formatterForKind (k : SyntaxNodeKind) : Formatter
+opaque formatterForKind (k : SyntaxNodeKind) : Formatter
 
 @[combinatorFormatter Lean.Parser.withAntiquot]
 def withAntiquot.formatter (antiP p : Formatter) : Formatter :=

stage0/src/Lean/PrettyPrinter/Parenthesizer.lean

@@ -258,14 +258,14 @@ def visitToken : Parenthesizer := do
 -- `categoryParser -> mkAntiquot -> termParser -> categoryParser`, so we need to introduce an indirection somewhere
 -- anyway.
 @[extern 8 "lean_mk_antiquot_parenthesizer"]
-constant mkAntiquot.parenthesizer' (name : String) (kind : Option SyntaxNodeKind) (anonymous := true) : Parenthesizer
+opaque mkAntiquot.parenthesizer' (name : String) (kind : Option SyntaxNodeKind) (anonymous := true) : Parenthesizer
 
 @[inline] def liftCoreM {α} (x : CoreM α) : ParenthesizerM α :=
   liftM x
 
 -- break up big mutual recursion
 @[extern "lean_pretty_printer_parenthesizer_interpret_parser_descr"]
-constant interpretParserDescr' : ParserDescr → CoreM Parenthesizer
+opaque interpretParserDescr' : ParserDescr → CoreM Parenthesizer
 
 unsafe def parenthesizerForKindUnsafe (k : SyntaxNodeKind) : Parenthesizer := do
   if k == `missing then
@@ -275,7 +275,7 @@ unsafe def parenthesizerForKindUnsafe (k : SyntaxNodeKind) : Parenthesizer := do
     p
 
 @[implementedBy parenthesizerForKindUnsafe]
-constant parenthesizerForKind (k : SyntaxNodeKind) : Parenthesizer
+opaque parenthesizerForKind (k : SyntaxNodeKind) : Parenthesizer
 
 @[combinatorParenthesizer Lean.Parser.withAntiquot]
 def withAntiquot.parenthesizer (antiP p : Parenthesizer) : Parenthesizer := do

stage0/src/Lean/Runtime.lean

@@ -7,10 +7,10 @@ Authors: Leonardo de Moura
 namespace Lean
 
 @[extern "lean_closure_max_args"]
-constant closureMaxArgsFn : Unit → Nat
+opaque closureMaxArgsFn : Unit → Nat
 
 @[extern "lean_max_small_nat"]
-constant maxSmallNatFn : Unit → Nat
+opaque maxSmallNatFn : Unit → Nat
 
 def closureMaxArgs : Nat :=
   closureMaxArgsFn ()

stage0/src/Lean/ScopedEnvExtension.lean

@@ -117,7 +117,7 @@ unsafe def registerScopedEnvExtensionUnsafe (descr : Descr α β σ) : IO (Scope
   return ext
 
 @[implementedBy registerScopedEnvExtensionUnsafe]
-constant registerScopedEnvExtension (descr : Descr α β σ) : IO (ScopedEnvExtension α β σ)
+opaque registerScopedEnvExtension (descr : Descr α β σ) : IO (ScopedEnvExtension α β σ)
 
 def ScopedEnvExtension.pushScope (ext : ScopedEnvExtension α β σ) (env : Environment) : Environment :=
   let s := ext.ext.getState env

stage0/src/Lean/Server/Rpc/Deriving.lean

@@ -26,14 +26,14 @@ private def deriveWithRefInstance (typeNm : Name) : CommandElabM Bool := do
       WithRpcRef.encodeUnsafe $(quote typeNm) r
 
     @[implementedBy encodeUnsafe]
-    constant encode [Monad m] [MonadRpcSession m] (r : WithRpcRef $typeId:ident) : m Lsp.RpcRef :=
+    opaque encode [Monad m] [MonadRpcSession m] (r : WithRpcRef $typeId:ident) : m Lsp.RpcRef :=
       pure ⟨0⟩
 
     unsafe def decodeUnsafe [Monad m] [MonadRpcSession m] (r : Lsp.RpcRef) : ExceptT String m (WithRpcRef $typeId:ident) :=
       WithRpcRef.decodeUnsafeAs $typeId:ident $(quote typeNm) r
 
     @[implementedBy decodeUnsafe]
-    constant decode [Monad m] [MonadRpcSession m] (r : Lsp.RpcRef) : ExceptT String m (WithRpcRef $typeId:ident) :=
+    opaque decode [Monad m] [MonadRpcSession m] (r : Lsp.RpcRef) : ExceptT String m (WithRpcRef $typeId:ident) :=
       throw "unreachable"
 
     instance : RpcEncoding (WithRpcRef $typeId:ident) Lsp.RpcRef :=
@@ -301,7 +301,7 @@ private unsafe def dispatchDeriveInstanceUnsafe (declNames : Array Name) (args?
     deriveInstance declNames[0]
 
 @[implementedBy dispatchDeriveInstanceUnsafe]
-private constant dispatchDeriveInstance (declNames : Array Name) (args? : Option Syntax) : CommandElabM Bool
+private opaque dispatchDeriveInstance (declNames : Array Name) (args? : Option Syntax) : CommandElabM Bool
 
 builtin_initialize
   Elab.registerBuiltinDerivingHandlerWithArgs ``RpcEncoding dispatchDeriveInstance

stage0/src/Lean/Server/Rpc/RequestHandling.lean

@@ -50,7 +50,7 @@ private unsafe def handleRpcCallUnsafe (p : Lsp.RpcCallParams) : RequestM (Reque
           message := s!"No RPC method '{p.method}' bound" }
 
 @[implementedBy handleRpcCallUnsafe]
-private constant handleRpcCall (p : Lsp.RpcCallParams) : RequestM (RequestTask Json)
+private opaque handleRpcCall (p : Lsp.RpcCallParams) : RequestM (RequestTask Json)
 
 builtin_initialize
   registerLspRequestHandler "$/lean/rpc/call" Lsp.RpcCallParams Json handleRpcCall

stage0/src/Lean/Util/FindExpr.lean

@@ -114,7 +114,7 @@ end FindExtImpl
   Similar to `find?`, but `p` can return `FindStep.done` to interrupt the search on subterms.
   Remark: Differently from `find?`, we do not invoke `p` for partial applications of an application. -/
 @[implementedBy FindExtImpl.findUnsafe?]
-constant findExt? (p : Expr → FindStep) (e : Expr) : Option Expr
+opaque findExt? (p : Expr → FindStep) (e : Expr) : Option Expr
 
 end Expr
 end Lean

stage0/src/Lean/Util/FoldConsts.lean

@@ -61,7 +61,7 @@ end FoldConstsImpl
 
 /-- Apply `f` to every constant occurring in `e` once. -/
 @[implementedBy FoldConstsImpl.foldUnsafe]
-constant foldConsts {α : Type} (e : Expr) (init : α) (f : Name → α → α) : α := init
+opaque foldConsts {α : Type} (e : Expr) (init : α) (f : Name → α → α) : α := init
 
 def getUsedConstants (e : Expr) : Array Name :=
   e.foldConsts #[] fun c cs => cs.push c

stage0/src/Lean/Util/HasConstCache.lean

@@ -32,6 +32,6 @@ where
   Return true iff `e` contains the constant `declName`.
   Remark: the results for visited expressions are stored in the state cache. -/
 @[implementedBy HasConstCache.containsUnsafe]
-constant HasConstCache.contains (e : Expr) : StateM (HasConstCache declName) Bool
+opaque HasConstCache.contains (e : Expr) : StateM (HasConstCache declName) Bool
 
 end Lean

stage0/src/Std/ShareCommon.lean

@@ -86,18 +86,18 @@ unsafe def ObjectPersistentSet.insert (s : ObjectPersistentSet) (o : Object) : O
   @PersistentHashSet.insert Object ⟨Object.eq⟩ ⟨Object.hash⟩ s o
 
 /- Internally `State` is implemented as a pair `ObjectMap` and `ObjectSet` -/
-constant StatePointed : NonemptyType
+opaque StatePointed : NonemptyType
 abbrev State : Type u := StatePointed.type
 @[extern "lean_sharecommon_mk_state"]
-constant mkState : Unit → State := fun _ => Classical.choice StatePointed.property
+opaque mkState : Unit → State := fun _ => Classical.choice StatePointed.property
 def State.empty : State := mkState ()
 instance State.inhabited : Inhabited State := ⟨State.empty⟩
 
 /- Internally `PersistentState` is implemented as a pair `ObjectPersistentMap` and `ObjectPersistentSet` -/
-constant PersistentStatePointed : NonemptyType
+opaque PersistentStatePointed : NonemptyType
 abbrev PersistentState : Type u := PersistentStatePointed.type
 @[extern "lean_sharecommon_mk_pstate"]
-constant mkPersistentState : Unit → PersistentState := fun _ => Classical.choice PersistentStatePointed.property
+opaque mkPersistentState : Unit → PersistentState := fun _ => Classical.choice PersistentStatePointed.property
 def PersistentState.empty : PersistentState := mkPersistentState ()
 instance PersistentState.inhabited : Inhabited PersistentState := ⟨PersistentState.empty⟩
 abbrev PState : Type u := PersistentState

stage0/stdlib/Lean/Elab/BuiltinCommand.c

@@ -17575,7 +17575,7 @@ _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = lean_unsigned_to_nat(358u);
-x_2 = lean_unsigned_to_nat(31u);
+x_2 = lean_unsigned_to_nat(29u);
 x_3 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_3, 0, x_1);
 lean_ctor_set(x_3, 1, x_2);
@@ -17589,7 +17589,7 @@ lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_obj
 x_1 = l___regBuiltin_Lean_Elab_Command_elabEval_declRange___closed__1;
 x_2 = lean_unsigned_to_nat(0u);
 x_3 = l___regBuiltin_Lean_Elab_Command_elabEval_declRange___closed__2;
-x_4 = lean_unsigned_to_nat(31u);
+x_4 = lean_unsigned_to_nat(29u);
 x_5 = lean_alloc_ctor(0, 4, 0);
 lean_ctor_set(x_5, 0, x_1);
 lean_ctor_set(x_5, 1, x_2);
@@ -17603,7 +17603,7 @@ _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = lean_unsigned_to_nat(358u);
-x_2 = lean_unsigned_to_nat(9u);
+x_2 = lean_unsigned_to_nat(7u);
 x_3 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_3, 0, x_1);
 lean_ctor_set(x_3, 1, x_2);
@@ -17615,7 +17615,7 @@ _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = lean_unsigned_to_nat(358u);
-x_2 = lean_unsigned_to_nat(17u);
+x_2 = lean_unsigned_to_nat(15u);
 x_3 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_3, 0, x_1);
 lean_ctor_set(x_3, 1, x_2);
@@ -17627,9 +17627,9 @@ _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; 
 x_1 = l___regBuiltin_Lean_Elab_Command_elabEval_declRange___closed__4;
-x_2 = lean_unsigned_to_nat(9u);
+x_2 = lean_unsigned_to_nat(7u);
 x_3 = l___regBuiltin_Lean_Elab_Command_elabEval_declRange___closed__5;
-x_4 = lean_unsigned_to_nat(17u);
+x_4 = lean_unsigned_to_nat(15u);
 x_5 = lean_alloc_ctor(0, 4, 0);
 lean_ctor_set(x_5, 0, x_1);
 lean_ctor_set(x_5, 1, x_2);

stage0/stdlib/Lean/Elab/DefView.c

@@ -33,7 +33,6 @@ lean_object* l_Lean_Syntax_getOptional_x3f(lean_object*);
 uint8_t l_Lean_Expr_isProp(lean_object*);
 static lean_object* l_Lean_Elab_Command_mkInstanceName___closed__1;
 LEAN_EXPORT lean_object* l___private_Lean_Elab_DefView_0__Lean_Elab_beqDefKind____x40_Lean_Elab_DefView___hyg_15____boxed(lean_object*, lean_object*);
-static lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1491____closed__1;
 lean_object* l_Lean_SourceInfo_fromRef(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Elab_Command_mkDefViewOfInstance___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_maxRecDepthErrorMessage;
@@ -41,7 +40,6 @@ LEAN_EXPORT lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_Comma
 LEAN_EXPORT lean_object* l_Lean_throwMaxRecDepthAt___at_Lean_Elab_Command_mkDefViewOfInstance___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_Elab_Command_mkDefViewOfInstance___closed__13;
 static lean_object* l_Lean_Elab_Command_mkDefViewOfOpaque___closed__3;
-static lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1491____closed__3;
 LEAN_EXPORT lean_object* l_Lean_MonadRef_mkInfoFromRefPos___at_Lean_Elab_Command_mkDefViewOfInstance___spec__11(lean_object*, lean_object*, lean_object*);
 lean_object* lean_st_ref_get(lean_object*, lean_object*);
 uint8_t lean_name_eq(lean_object*, lean_object*);
@@ -49,15 +47,12 @@ static lean_object* l_Lean_Elab_Command_mkDefViewOfInstance___closed__1;
 lean_object* l_Lean_mkIdentFrom(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Elab_Command_mkInstanceName___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_toSubarray___rarg(lean_object*, lean_object*, lean_object*);
-static lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1491____closed__4;
 lean_object* lean_array_push(lean_object*, lean_object*);
 lean_object* lean_array_get_size(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_Elab_Command_mkDefViewOfInstance___spec__3(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_string_append(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Elab_Command_mkInstanceName___lambda__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_Elab_Command_mkDefViewOfAbbrev___closed__1;
-static lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1491____closed__2;
-static lean_object* l_Lean_Elab_Command_isDefLike___closed__12;
 LEAN_EXPORT lean_object* l_Lean_Elab_Command_mkInstanceName___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Elab_Command_mkDefViewOfOpaque(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_synthesizeSyntheticMVars(uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -146,7 +141,6 @@ static lean_object* l_Lean_Elab_Command_mkDefViewOfInstance___closed__6;
 size_t lean_usize_of_nat(lean_object*);
 LEAN_EXPORT uint8_t l_Lean_Elab_DefKind_isTheorem(uint8_t);
 LEAN_EXPORT lean_object* l_Lean_Elab_Command_mkFreshInstanceName(lean_object*);
-static lean_object* l_Lean_Elab_Command_isDefLike___closed__13;
 LEAN_EXPORT lean_object* l_Lean_Elab_Command_mkInstanceName___lambda__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_Command_mkDefViewOfInstance___spec__5(lean_object*, lean_object*);
 static lean_object* l_Lean_Elab_Command_mkDefViewOfOpaque___closed__7;
@@ -172,12 +166,13 @@ lean_object* l_Lean_Syntax_getKind(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Elab_Command_mkInstanceName(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Elab_Command_mkFreshInstanceName___boxed(lean_object*);
 static lean_object* l_Lean_throwMaxRecDepthAt___at_Lean_Elab_Command_mkInstanceName___spec__4___closed__1;
-LEAN_EXPORT lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1491_(lean_object*);
+LEAN_EXPORT lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1469_(lean_object*);
 static lean_object* l_Lean_Elab_Command_mkInstanceName___closed__3;
 LEAN_EXPORT lean_object* l_Lean_Elab_liftMacroM___at_Lean_Elab_Command_mkInstanceName___spec__1___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_throwMaxRecDepthAt___at_Lean_Elab_Command_mkInstanceName___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_ReaderT_pure___at_Lean_Elab_liftMacroM___spec__2___rarg___boxed(lean_object*, lean_object*, lean_object*);
 static lean_object* l_Lean_throwMaxRecDepthAt___at_Lean_Elab_Command_mkInstanceName___spec__4___closed__2;
+static lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1469____closed__2;
 static lean_object* l_Lean_Elab_Command_isDefLike___closed__6;
 lean_object* l_Lean_Elab_Command_getMainModule___rarg(lean_object*, lean_object*);
 static lean_object* l_Lean_Elab_Command_mkInstanceName___lambda__1___closed__3;
@@ -193,6 +188,7 @@ LEAN_EXPORT lean_object* l_Lean_throwError___at_Lean_Elab_Command_mkDefView___sp
 uint8_t l_Lean_Syntax_isNone(lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_Command_mkDefViewOfInstance___spec__10(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Modifiers_addAttribute(lean_object*, lean_object*);
+static lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1469____closed__3;
 static lean_object* l_Lean_Elab_Command_mkInstanceName___lambda__2___closed__1;
 static lean_object* l_Lean_Elab_Command_mkDefViewOfInstance___closed__9;
 lean_object* l_Lean_Meta_instantiateMVars(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -218,6 +214,7 @@ static lean_object* l_Lean_Elab_Command_mkDefViewOfOpaque___lambda__2___closed__
 static lean_object* l_Lean_Elab_Command_mkDefViewOfInstance___closed__18;
 lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Elab_liftMacroM___at_Lean_Elab_Command_mkInstanceName___spec__1___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*);
+static lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1469____closed__4;
 LEAN_EXPORT lean_object* l_Lean_Elab_Command_mkDefView(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Elab_liftMacroM___at_Lean_Elab_Command_mkInstanceName___spec__1___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 LEAN_EXPORT lean_object* l_Lean_Elab_liftMacroM___at_Lean_Elab_Command_mkInstanceName___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
@@ -232,6 +229,7 @@ LEAN_EXPORT lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_Comma
 static lean_object* l_Lean_Elab_Command_mkDefViewOfOpaque___closed__6;
 lean_object* l_Lean_Elab_Command_getScope___rarg(lean_object*, lean_object*);
 static lean_object* l_Lean_Elab_Command_mkDefViewOfInstance___closed__14;
+static lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1469____closed__1;
 static lean_object* l_Lean_Elab_instInhabitedDefView___closed__2;
 static lean_object* l_Lean_Elab_Command_mkDefViewOfInstance___closed__5;
 LEAN_EXPORT lean_object* l_Lean_Elab_DefView_deriving_x3f___default;
@@ -4131,7 +4129,7 @@ static lean_object* _init_l_Lean_Elab_Command_isDefLike___closed__7() {
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_mk_string_from_bytes("constant", 8);
+x_1 = lean_mk_string_from_bytes("opaque", 6);
 return x_1;
 }
 }
@@ -4148,24 +4146,6 @@ return x_3;
 static lean_object* _init_l_Lean_Elab_Command_isDefLike___closed__9() {
 _start:
 {
-lean_object* x_1; 
-x_1 = lean_mk_string_from_bytes("opaque", 6);
-return x_1;
-}
-}
-static lean_object* _init_l_Lean_Elab_Command_isDefLike___closed__10() {
-_start:
-{
-lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Elab_Command_mkDefViewOfInstance___closed__15;
-x_2 = l_Lean_Elab_Command_isDefLike___closed__9;
-x_3 = lean_name_mk_string(x_1, x_2);
-return x_3;
-}
-}
-static lean_object* _init_l_Lean_Elab_Command_isDefLike___closed__11() {
-_start:
-{
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_Elab_Command_mkDefViewOfInstance___closed__15;
 x_2 = l_Lean_Elab_Command_mkDefViewOfInstance___closed__7;
@@ -4173,7 +4153,7 @@ x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
 }
 }
-static lean_object* _init_l_Lean_Elab_Command_isDefLike___closed__12() {
+static lean_object* _init_l_Lean_Elab_Command_isDefLike___closed__10() {
 _start:
 {
 lean_object* x_1; 
@@ -4181,12 +4161,12 @@ x_1 = lean_mk_string_from_bytes("example", 7);
 return x_1;
 }
 }
-static lean_object* _init_l_Lean_Elab_Command_isDefLike___closed__13() {
+static lean_object* _init_l_Lean_Elab_Command_isDefLike___closed__11() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_Elab_Command_mkDefViewOfInstance___closed__15;
-x_2 = l_Lean_Elab_Command_isDefLike___closed__12;
+x_2 = l_Lean_Elab_Command_isDefLike___closed__10;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
 }
@@ -4216,21 +4196,32 @@ x_10 = lean_name_eq(x_2, x_9);
 if (x_10 == 0)
 {
 lean_object* x_11; uint8_t x_12; 
-x_11 = l_Lean_Elab_Command_isDefLike___closed__10;
+x_11 = l_Lean_Elab_Command_isDefLike___closed__9;
 x_12 = lean_name_eq(x_2, x_11);
 if (x_12 == 0)
 {
 lean_object* x_13; uint8_t x_14; 
 x_13 = l_Lean_Elab_Command_isDefLike___closed__11;
 x_14 = lean_name_eq(x_2, x_13);
-if (x_14 == 0)
-{
-lean_object* x_15; uint8_t x_16; 
-x_15 = l_Lean_Elab_Command_isDefLike___closed__13;
-x_16 = lean_name_eq(x_2, x_15);
 lean_dec(x_2);
+return x_14;
+}
+else
+{
+uint8_t x_15; 
+lean_dec(x_2);
+x_15 = 1;
+return x_15;
+}
+}
+else
+{
+uint8_t x_16; 
+lean_dec(x_2);
+x_16 = 1;
 return x_16;
 }
+}
 else
 {
 uint8_t x_17; 
@@ -4255,30 +4246,6 @@ x_19 = 1;
 return x_19;
 }
 }
-else
-{
-uint8_t x_20; 
-lean_dec(x_2);
-x_20 = 1;
-return x_20;
-}
-}
-else
-{
-uint8_t x_21; 
-lean_dec(x_2);
-x_21 = 1;
-return x_21;
-}
-}
-else
-{
-uint8_t x_22; 
-lean_dec(x_2);
-x_22 = 1;
-return x_22;
-}
-}
 }
 LEAN_EXPORT lean_object* l_Lean_Elab_Command_isDefLike___boxed(lean_object* x_1) {
 _start:
@@ -4386,102 +4353,89 @@ x_14 = lean_name_eq(x_6, x_13);
 if (x_14 == 0)
 {
 lean_object* x_15; uint8_t x_16; 
-x_15 = l_Lean_Elab_Command_isDefLike___closed__10;
+x_15 = l_Lean_Elab_Command_isDefLike___closed__9;
 x_16 = lean_name_eq(x_6, x_15);
 if (x_16 == 0)
 {
 lean_object* x_17; uint8_t x_18; 
 x_17 = l_Lean_Elab_Command_isDefLike___closed__11;
 x_18 = lean_name_eq(x_6, x_17);
+lean_dec(x_6);
 if (x_18 == 0)
 {
-lean_object* x_19; uint8_t x_20; 
-x_19 = l_Lean_Elab_Command_isDefLike___closed__13;
-x_20 = lean_name_eq(x_6, x_19);
-lean_dec(x_6);
-if (x_20 == 0)
-{
-lean_object* x_21; lean_object* x_22; 
+lean_object* x_19; lean_object* x_20; 
 lean_dec(x_2);
 lean_dec(x_1);
-x_21 = l_Lean_Elab_Command_mkDefView___closed__2;
-x_22 = l_Lean_throwError___at_Lean_Elab_Command_mkDefView___spec__1(x_21, x_3, x_4, x_5);
+x_19 = l_Lean_Elab_Command_mkDefView___closed__2;
+x_20 = l_Lean_throwError___at_Lean_Elab_Command_mkDefView___spec__1(x_19, x_3, x_4, x_5);
 lean_dec(x_4);
-return x_22;
+return x_20;
 }
 else
 {
-lean_object* x_23; lean_object* x_24; 
+lean_object* x_21; lean_object* x_22; 
 lean_dec(x_4);
 lean_dec(x_3);
-x_23 = l_Lean_Elab_Command_mkDefViewOfExample(x_1, x_2);
-x_24 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_24, 0, x_23);
-lean_ctor_set(x_24, 1, x_5);
+x_21 = l_Lean_Elab_Command_mkDefViewOfExample(x_1, x_2);
+x_22 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_22, 0, x_21);
+lean_ctor_set(x_22, 1, x_5);
+return x_22;
+}
+}
+else
+{
+lean_object* x_23; 
+lean_dec(x_6);
+x_23 = l_Lean_Elab_Command_mkDefViewOfInstance(x_1, x_2, x_3, x_4, x_5);
+return x_23;
+}
+}
+else
+{
+lean_object* x_24; 
+lean_dec(x_6);
+x_24 = l_Lean_Elab_Command_mkDefViewOfOpaque(x_1, x_2, x_3, x_4, x_5);
 return x_24;
 }
 }
 else
 {
-lean_object* x_25; 
+lean_object* x_25; lean_object* x_26; 
 lean_dec(x_6);
-x_25 = l_Lean_Elab_Command_mkDefViewOfInstance(x_1, x_2, x_3, x_4, x_5);
-return x_25;
-}
-}
-else
-{
-lean_object* x_26; 
-lean_dec(x_6);
-x_26 = l_Lean_Elab_Command_mkDefViewOfOpaque(x_1, x_2, x_3, x_4, x_5);
+lean_dec(x_4);
+lean_dec(x_3);
+x_25 = l_Lean_Elab_Command_mkDefViewOfTheorem(x_1, x_2);
+x_26 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_26, 0, x_25);
+lean_ctor_set(x_26, 1, x_5);
 return x_26;
 }
 }
 else
 {
-lean_object* x_27; 
+lean_object* x_27; lean_object* x_28; 
 lean_dec(x_6);
-x_27 = l_Lean_Elab_Command_mkDefViewOfOpaque(x_1, x_2, x_3, x_4, x_5);
-return x_27;
+lean_dec(x_4);
+lean_dec(x_3);
+x_27 = l_Lean_Elab_Command_mkDefViewOfDef(x_1, x_2);
+x_28 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_28, 0, x_27);
+lean_ctor_set(x_28, 1, x_5);
+return x_28;
 }
 }
 else
 {
-lean_object* x_28; lean_object* x_29; 
+lean_object* x_29; lean_object* x_30; 
 lean_dec(x_6);
 lean_dec(x_4);
 lean_dec(x_3);
-x_28 = l_Lean_Elab_Command_mkDefViewOfTheorem(x_1, x_2);
-x_29 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_29, 0, x_28);
-lean_ctor_set(x_29, 1, x_5);
-return x_29;
-}
-}
-else
-{
-lean_object* x_30; lean_object* x_31; 
-lean_dec(x_6);
-lean_dec(x_4);
-lean_dec(x_3);
-x_30 = l_Lean_Elab_Command_mkDefViewOfDef(x_1, x_2);
-x_31 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_31, 0, x_30);
-lean_ctor_set(x_31, 1, x_5);
-return x_31;
-}
-}
-else
-{
-lean_object* x_32; lean_object* x_33; 
-lean_dec(x_6);
-lean_dec(x_4);
-lean_dec(x_3);
-x_32 = l_Lean_Elab_Command_mkDefViewOfAbbrev(x_1, x_2);
-x_33 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_33, 0, x_32);
-lean_ctor_set(x_33, 1, x_5);
-return x_33;
+x_29 = l_Lean_Elab_Command_mkDefViewOfAbbrev(x_1, x_2);
+x_30 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_30, 0, x_29);
+lean_ctor_set(x_30, 1, x_5);
+return x_30;
 }
 }
 }
@@ -4494,7 +4448,7 @@ lean_dec(x_3);
 return x_5;
 }
 }
-static lean_object* _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1491____closed__1() {
+static lean_object* _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1469____closed__1() {
 _start:
 {
 lean_object* x_1; 
@@ -4502,17 +4456,17 @@ x_1 = lean_mk_string_from_bytes("Elab", 4);
 return x_1;
 }
 }
-static lean_object* _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1491____closed__2() {
+static lean_object* _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1469____closed__2() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = lean_box(0);
-x_2 = l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1491____closed__1;
+x_2 = l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1469____closed__1;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
 }
 }
-static lean_object* _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1491____closed__3() {
+static lean_object* _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1469____closed__3() {
 _start:
 {
 lean_object* x_1; 
@@ -4520,21 +4474,21 @@ x_1 = lean_mk_string_from_bytes("definition", 10);
 return x_1;
 }
 }
-static lean_object* _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1491____closed__4() {
+static lean_object* _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1469____closed__4() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1491____closed__2;
-x_2 = l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1491____closed__3;
+x_1 = l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1469____closed__2;
+x_2 = l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1469____closed__3;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
 }
 }
-LEAN_EXPORT lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1491_(lean_object* x_1) {
+LEAN_EXPORT lean_object* l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1469_(lean_object* x_1) {
 _start:
 {
 lean_object* x_2; lean_object* x_3; 
-x_2 = l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1491____closed__4;
+x_2 = l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1469____closed__4;
 x_3 = l_Lean_registerTraceClass(x_2, x_1);
 return x_3;
 }
@@ -4725,23 +4679,19 @@ l_Lean_Elab_Command_isDefLike___closed__10 = _init_l_Lean_Elab_Command_isDefLike
 lean_mark_persistent(l_Lean_Elab_Command_isDefLike___closed__10);
 l_Lean_Elab_Command_isDefLike___closed__11 = _init_l_Lean_Elab_Command_isDefLike___closed__11();
 lean_mark_persistent(l_Lean_Elab_Command_isDefLike___closed__11);
-l_Lean_Elab_Command_isDefLike___closed__12 = _init_l_Lean_Elab_Command_isDefLike___closed__12();
-lean_mark_persistent(l_Lean_Elab_Command_isDefLike___closed__12);
-l_Lean_Elab_Command_isDefLike___closed__13 = _init_l_Lean_Elab_Command_isDefLike___closed__13();
-lean_mark_persistent(l_Lean_Elab_Command_isDefLike___closed__13);
 l_Lean_Elab_Command_mkDefView___closed__1 = _init_l_Lean_Elab_Command_mkDefView___closed__1();
 lean_mark_persistent(l_Lean_Elab_Command_mkDefView___closed__1);
 l_Lean_Elab_Command_mkDefView___closed__2 = _init_l_Lean_Elab_Command_mkDefView___closed__2();
 lean_mark_persistent(l_Lean_Elab_Command_mkDefView___closed__2);
-l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1491____closed__1 = _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1491____closed__1();
-lean_mark_persistent(l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1491____closed__1);
-l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1491____closed__2 = _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1491____closed__2();
-lean_mark_persistent(l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1491____closed__2);
-l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1491____closed__3 = _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1491____closed__3();
-lean_mark_persistent(l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1491____closed__3);
-l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1491____closed__4 = _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1491____closed__4();
-lean_mark_persistent(l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1491____closed__4);
-res = l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1491_(lean_io_mk_world());
+l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1469____closed__1 = _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1469____closed__1();
+lean_mark_persistent(l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1469____closed__1);
+l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1469____closed__2 = _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1469____closed__2();
+lean_mark_persistent(l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1469____closed__2);
+l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1469____closed__3 = _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1469____closed__3();
+lean_mark_persistent(l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1469____closed__3);
+l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1469____closed__4 = _init_l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1469____closed__4();
+lean_mark_persistent(l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1469____closed__4);
+res = l_Lean_Elab_Command_initFn____x40_Lean_Elab_DefView___hyg_1469_(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
 return lean_io_result_mk_ok(lean_box(0));

stage0/stdlib/Lean/Elab/Print.c

@@ -1879,7 +1879,7 @@ static lean_object* _init_l___private_Lean_Elab_Print_0__Lean_Elab_Command_print
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_mk_string_from_bytes("constant", 8);
+x_1 = lean_mk_string_from_bytes("opaque", 6);
 return x_1;
 }
 }

stage0/stdlib/Lean/Linter/Basic.c

@@ -1863,7 +1863,7 @@ static lean_object* _init_l_Lean_Linter_unusedVariables_isInConstantOrAxiom___ra
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_mk_string_from_bytes("constant", 8);
+x_1 = lean_mk_string_from_bytes("opaque", 6);
 return x_1;
 }
 }

stage0/stdlib/Lean/Server/Rpc/Deriving.c

@@ -2157,7 +2157,7 @@ static lean_object* _init_l___private_Lean_Server_Rpc_Deriving_0__Lean_Server_Rp
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_mk_string_from_bytes("constant", 8);
+x_1 = lean_mk_string_from_bytes("opaque", 6);
 return x_1;
 }
 }