chore: update Pi instance names (#5447)

Override instance names for nonempty / inhabited / subsingleton arrows,
per
[zulip](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Pi.20instance.20names.20in.20Lean.204.20core/near/466248246).
This commit is contained in:
Kim Morrison 2024-09-24 14:12:51 +10:00 committed by GitHub
parent 0cae7165aa
commit 6b0d4e50c0
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 6 additions and 3 deletions

View file

@ -1897,7 +1897,8 @@ theorem funext {α : Sort u} {β : α → Sort v} {f g : (x : α) → β x}
show extfunApp (Quot.mk eqv f) = extfunApp (Quot.mk eqv g)
exact congrArg extfunApp (Quot.sound h)
instance {α : Sort u} {β : α → Sort v} [∀ a, Subsingleton (β a)] : Subsingleton (∀ a, β a) where
instance Pi.instSubsingleton {α : Sort u} {β : α → Sort v} [∀ a, Subsingleton (β a)] :
Subsingleton (∀ a, β a) where
allEq f g := funext fun a => Subsingleton.elim (f a) (g a)
/-! # Squash -/

View file

@ -757,7 +757,8 @@ noncomputable def Classical.ofNonempty {α : Sort u} [Nonempty α] : α :=
instance (α : Sort u) {β : Sort v} [Nonempty β] : Nonempty (α → β) :=
Nonempty.intro fun _ => Classical.ofNonempty
instance (α : Sort u) {β : α → Sort v} [(a : α) → Nonempty (β a)] : Nonempty ((a : α) → β a) :=
instance Pi.instNonempty (α : Sort u) {β : α → Sort v} [(a : α) → Nonempty (β a)] :
Nonempty ((a : α) → β a) :=
Nonempty.intro fun _ => Classical.ofNonempty
instance : Inhabited (Sort u) where
@ -766,7 +767,8 @@ instance : Inhabited (Sort u) where
instance (α : Sort u) {β : Sort v} [Inhabited β] : Inhabited (α → β) where
default := fun _ => default
instance (α : Sort u) {β : α → Sort v} [(a : α) → Inhabited (β a)] : Inhabited ((a : α) → β a) where
instance Pi.instInhabited (α : Sort u) {β : α → Sort v} [(a : α) → Inhabited (β a)] :
Inhabited ((a : α) → β a) where
default := fun _ => default
deriving instance Inhabited for Bool