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

chore: rename PointedType => NonemptyType

Browse source
This commit is contained in:
Leonardo de Moura 2022-01-15 11:42:09 -08:00
parent f3d8fcc85d
commit 4ac34f4cd5
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
Lake/Config/Opaque.lean
View file

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