From 4ac34f4cd5818c1fac8af438b415eeb7243ce2d8 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 15 Jan 2022 11:42:09 -0800 Subject: [PATCH] chore: rename `PointedType` => `NonemptyType` --- Lake/Config/Opaque.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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