diff --git a/Lake/Config/Opaque.lean b/Lake/Config/Opaque.lean index b1489e1d72..849270a8ae 100644 --- a/Lake/Config/Opaque.lean +++ b/Lake/Config/Opaque.lean @@ -5,14 +5,14 @@ Authors: Mac Malone -/ namespace Lake -constant OpaquePackagePointed : PointedType.{0} +constant OpaquePackagePointed : NonemptyType.{0} /-- Opaque reference to a `Package` used for forward declaration. -/ def OpaquePackage : Type := OpaquePackagePointed.type instance : Nonempty OpaquePackage := OpaquePackagePointed.property -constant OpaqueWorkspacePointed : PointedType.{0} +constant OpaqueWorkspacePointed : NonemptyType.{0} /-- Opaque reference to a `Workspace` used for forward declaration. -/ def OpaqueWorkspace : Type := OpaqueWorkspacePointed.type