From e880dd52a4936038a4fc00dc4ea4ce02f99ba12f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 14 Jan 2022 20:37:46 -0800 Subject: [PATCH] chore: `PointedType` --- Lake/Config/Opaque.lean | 4 ++++ Lake/Config/Package.lean | 3 +-- Lake/Config/Workspace.lean | 3 +-- 3 files changed, 6 insertions(+), 4 deletions(-) diff --git a/Lake/Config/Opaque.lean b/Lake/Config/Opaque.lean index 855917af80..b1489e1d72 100644 --- a/Lake/Config/Opaque.lean +++ b/Lake/Config/Opaque.lean @@ -10,7 +10,11 @@ constant OpaquePackagePointed : PointedType.{0} /-- Opaque reference to a `Package` used for forward declaration. -/ def OpaquePackage : Type := OpaquePackagePointed.type +instance : Nonempty OpaquePackage := OpaquePackagePointed.property + constant OpaqueWorkspacePointed : PointedType.{0} /-- Opaque reference to a `Workspace` used for forward declaration. -/ def OpaqueWorkspace : Type := OpaqueWorkspacePointed.type + +instance : Nonempty OpaqueWorkspace := OpaqueWorkspacePointed.property diff --git a/Lake/Config/Package.lean b/Lake/Config/Package.lean index 9fd8b06708..7c2b9cbb77 100644 --- a/Lake/Config/Package.lean +++ b/Lake/Config/Package.lean @@ -289,8 +289,7 @@ namespace OpaquePackage unsafe def unsafeMk (pkg : Package) : OpaquePackage := unsafeCast pkg -@[implementedBy unsafeMk] constant mk (pkg : Package) : OpaquePackage := - OpaquePackagePointed.val +@[implementedBy unsafeMk] constant mk (pkg : Package) : OpaquePackage instance : Coe Package OpaquePackage := ⟨mk⟩ instance : Inhabited OpaquePackage := ⟨mk Inhabited.default⟩ diff --git a/Lake/Config/Workspace.lean b/Lake/Config/Workspace.lean index dfdaa0e23a..625771013a 100644 --- a/Lake/Config/Workspace.lean +++ b/Lake/Config/Workspace.lean @@ -28,8 +28,7 @@ namespace OpaqueWorkspace unsafe def unsafeMk (ws : Workspace) : OpaqueWorkspace := unsafeCast ws -@[implementedBy unsafeMk] constant mk (ws : Workspace) : OpaqueWorkspace := - OpaqueWorkspacePointed.val +@[implementedBy unsafeMk] constant mk (ws : Workspace) : OpaqueWorkspace instance : Coe Workspace OpaqueWorkspace := ⟨mk⟩ instance : Inhabited OpaqueWorkspace := ⟨mk Inhabited.default⟩