chore: replace constant with opaque

Lake/Config/Load.lean

@@ -132,5 +132,5 @@ Load the package located in
 the given directory with the given configuration file.
 -/
 @[implementedBy loadUnsafe]
-constant load (dir : FilePath) (args : List String := [])
+opaque load (dir : FilePath) (args : List String := [])
 (configFile := dir / defaultConfigFile) (leanOpts := Options.empty) : LogT IO Package

Lake/Config/Opaque.lean

@@ -5,14 +5,14 @@ Authors: Mac Malone
 -/
 namespace Lake
 
-constant OpaquePackagePointed : NonemptyType.{0}
+opaque OpaquePackagePointed : NonemptyType.{0}
 
 /-- Opaque reference to a `Package` used for forward declaration. -/
 def OpaquePackage : Type := OpaquePackagePointed.type
 
 instance : Nonempty OpaquePackage := OpaquePackagePointed.property
 
-constant OpaqueWorkspacePointed : NonemptyType.{0}
+opaque OpaqueWorkspacePointed : NonemptyType.{0}
 
 /-- Opaque reference to a `Workspace` used for forward declaration. -/
 def OpaqueWorkspace : Type := OpaqueWorkspacePointed.type

Lake/Config/Package.lean

@@ -285,7 +285,7 @@ namespace OpaquePackage
 unsafe def unsafeMk (pkg : Package) : OpaquePackage :=
   unsafeCast pkg
 
-@[implementedBy unsafeMk] constant mk (pkg : Package) : OpaquePackage
+@[implementedBy unsafeMk] opaque mk (pkg : Package) : OpaquePackage
 
 instance : Coe Package OpaquePackage := ⟨mk⟩
 instance : Inhabited OpaquePackage := ⟨mk Inhabited.default⟩
@@ -293,7 +293,7 @@ instance : Inhabited OpaquePackage := ⟨mk Inhabited.default⟩
 unsafe def unsafeGet (self : OpaquePackage) : Package :=
   unsafeCast self
 
-@[implementedBy unsafeGet] constant get (self : OpaquePackage) : Package
+@[implementedBy unsafeGet] opaque get (self : OpaquePackage) : Package
 
 instance : Coe OpaquePackage Package := ⟨get⟩
 

Lake/Config/Workspace.lean

@@ -30,7 +30,7 @@ namespace OpaqueWorkspace
 unsafe def unsafeMk (ws : Workspace) : OpaqueWorkspace :=
   unsafeCast ws
 
-@[implementedBy unsafeMk] constant mk (ws : Workspace) : OpaqueWorkspace
+@[implementedBy unsafeMk] opaque mk (ws : Workspace) : OpaqueWorkspace
 
 instance : Coe Workspace OpaqueWorkspace := ⟨mk⟩
 instance : Inhabited OpaqueWorkspace := ⟨mk Inhabited.default⟩
@@ -38,7 +38,7 @@ instance : Inhabited OpaqueWorkspace := ⟨mk Inhabited.default⟩
 unsafe def unsafeGet (self : OpaqueWorkspace) : Workspace :=
   unsafeCast self
 
-@[implementedBy unsafeGet] constant get (self : OpaqueWorkspace) : Workspace
+@[implementedBy unsafeGet] opaque get (self : OpaqueWorkspace) : Workspace
 
 instance : Coe OpaqueWorkspace Workspace := ⟨get⟩
 

Lake/DSL/Config.lean

@@ -13,13 +13,13 @@ open Lean Elab Term
 A dummy default constant for `__dir__` to make it type check
 outside Lakefile elaboration (e.g., when editing).
 -/
-constant dummyDir : System.FilePath
+opaque dummyDir : System.FilePath
 
 /--
 A dummy default constant for `__args__` to make it type check
 outside Lakefile elaboration (e.g., when editing).
 -/
-constant dummyArgs : List String
+opaque dummyArgs : List String
 
 /--
 A macro that expands to the path of package's directory

Lake/Util/EvalTerm.lean

@@ -38,7 +38,7 @@ unsafe def unsafeEvalTerm (α) [ToExpr α] (term : Syntax) : TermElabM α := do
     setEnv env
 
 @[implementedBy unsafeEvalTerm]
-constant evalTerm (α) [ToExpr α] (term : Syntax) : TermElabM α
+opaque evalTerm (α) [ToExpr α] (term : Syntax) : TermElabM α
 
 -- ## ToExpr Instances
 

examples/ffi/lib/lean/FFI.lean

@@ -1,5 +1,5 @@
 @[extern "my_add"]
-constant myAdd : UInt32 → UInt32 → UInt32
+opaque myAdd : UInt32 → UInt32 → UInt32
 
 @[extern "my_lean_fun"]
-constant myLeanFun : IO PUnit
+opaque myLeanFun : IO PUnit