max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: PointedType

Browse source
This commit is contained in:
Leonardo de Moura 2022-01-14 20:37:46 -08:00
parent 752bc24f78
commit e880dd52a4
3 changed files with 6 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
Lake/Config/Opaque.lean
View file

@ -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

3
Lake/Config/Package.lean
View file

@ -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⟩

3
Lake/Config/Workspace.lean
View file

@ -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⟩