chore: rename PointedType => NonemptyType

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
 

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

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
 

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

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