From b0d9c16c7a8c4525570027c694f030b54d53ffb8 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 15 Jan 2022 11:41:38 -0800
Subject: [PATCH] chore: rename `PointedType` => `NonemptyType`

---
 src/Init/Prelude.lean     | 8 ++++----
 src/Init/System/ST.lean   | 2 +-
 src/Lean/Environment.lean | 2 +-
 src/Std/ShareCommon.lean  | 4 ++--
 tests/lean/run/1385.lean  | 2 +-
 5 files changed, 9 insertions(+), 9 deletions(-)

diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index 4b18940b5a..487a63c51f 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -242,12 +242,12 @@ theorem PLift.down_up {α : Sort u} (a : α) : Eq (down (up a)) a :=
   rfl
 
 /- Pointed types -/
-def PointedType := Subtype fun α : Type u => Nonempty α
+def NonemptyType := Subtype fun α : Type u => Nonempty α
 
-abbrev PointedType.type (type : PointedType.{u}) : Type u :=
+abbrev NonemptyType.type (type : NonemptyType.{u}) : Type u :=
   type.val
 
-instance : Inhabited PointedType.{u} where
+instance : Inhabited NonemptyType.{u} where
   default := ⟨PUnit.{u+1}, Nonempty.intro ⟨⟩⟩
 
 /-- Universe lifting operation -/
@@ -2164,7 +2164,7 @@ def maxRecDepthErrorMessage : String :=
 namespace Macro
 
 /- References -/
-private constant MethodsRefPointed : PointedType.{0}
+private constant MethodsRefPointed : NonemptyType.{0}
 
 private def MethodsRef : Type := MethodsRefPointed.type
 
diff --git a/src/Init/System/ST.lean b/src/Init/System/ST.lean
index cda87cdae5..e25d3de949 100644
--- a/src/Init/System/ST.lean
+++ b/src/Init/System/ST.lean
@@ -42,7 +42,7 @@ instance {ε σ} : MonadLift (ST σ) (EST ε σ) := ⟨fun x s =>
 namespace ST
 
 /- References -/
-constant RefPointed : PointedType.{0}
+constant RefPointed : NonemptyType.{0}
 
 structure Ref (σ : Type) (α : Type) : Type where
   ref : RefPointed.type
diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean
index 752f46ee55..7a1ae261ce 100644
--- a/src/Lean/Environment.lean
+++ b/src/Lean/Environment.lean
@@ -44,7 +44,7 @@ constant CompactedRegion.isMemoryMapped : CompactedRegion → Bool
 unsafe constant CompactedRegion.free : CompactedRegion → IO Unit
 
 /- Opaque persistent environment extension entry. -/
-constant EnvExtensionEntrySpec : PointedType.{0}
+constant EnvExtensionEntrySpec : NonemptyType.{0}
 def EnvExtensionEntry : Type := EnvExtensionEntrySpec.type
 instance : Nonempty EnvExtensionEntry := EnvExtensionEntrySpec.property
 
diff --git a/src/Std/ShareCommon.lean b/src/Std/ShareCommon.lean
index 4dc213f923..07694cf9c2 100644
--- a/src/Std/ShareCommon.lean
+++ b/src/Std/ShareCommon.lean
@@ -86,7 +86,7 @@ unsafe def ObjectPersistentSet.insert (s : ObjectPersistentSet) (o : Object) : O
   @PersistentHashSet.insert Object ⟨Object.eq⟩ ⟨Object.hash⟩ s o
 
 /- Internally `State` is implemented as a pair `ObjectMap` and `ObjectSet` -/
-constant StatePointed : PointedType
+constant StatePointed : NonemptyType
 abbrev State : Type u := StatePointed.type
 @[extern "lean_sharecommon_mk_state"]
 constant mkState : Unit → State := fun _ => Classical.choice StatePointed.property
@@ -94,7 +94,7 @@ def State.empty : State := mkState ()
 instance State.inhabited : Inhabited State := ⟨State.empty⟩
 
 /- Internally `PersistentState` is implemented as a pair `ObjectPersistentMap` and `ObjectPersistentSet` -/
-constant PersistentStatePointed : PointedType
+constant PersistentStatePointed : NonemptyType
 abbrev PersistentState : Type u := PersistentStatePointed.type
 @[extern "lean_sharecommon_mk_pstate"]
 constant mkPersistentState : Unit → PersistentState := fun _ => Classical.choice PersistentStatePointed.property
diff --git a/tests/lean/run/1385.lean b/tests/lean/run/1385.lean
index d2dce979ad..5ee3c949c9 100644
--- a/tests/lean/run/1385.lean
+++ b/tests/lean/run/1385.lean
@@ -1,5 +1,5 @@
 def S := List Nat
-constant TSpec : PointedType
+constant TSpec : NonemptyType
 def T (s : S) : Type :=  TSpec.type
 instance (s : S) : Nonempty (T s) :=
   TSpec.property