From 20ef9097198a78a6a8d27a4b2d23545d1b68c66e Mon Sep 17 00:00:00 2001
From: Bolton Bailey <bolton.bailey@gmail.com>
Date: Thu, 10 Feb 2022 13:11:45 +0000
Subject: [PATCH] feat(data/part): add instances (#11868)

Add common instances for `part \alpha` to be inherited from `\alpha`. Spun off of #11046



Co-authored-by: YaelDillies <yael.dillies@gmail.com>
---
 src/computability/halting.lean |  2 ++
 src/data/part.lean             | 20 ++++++++++++++++++++
 2 files changed, 22 insertions(+)

diff --git a/src/computability/halting.lean b/src/computability/halting.lean
index 39f8f73569e8e..0f0f670810b66 100644
--- a/src/computability/halting.lean
+++ b/src/computability/halting.lean
@@ -301,6 +301,8 @@ protected theorem map {n f} {g : vector ℕ (n+1) → ℕ}
 by simp [(part.bind_some_eq_map _ _).symm];
    exact hf.bind hg
 
+local attribute [-instance] part.has_zero
+
 /-- Analogous to `nat.partrec'` for `ℕ`-valued functions, a predicate for partial recursive
   vector-valued functions.-/
 def vec {n m} (f : vector ℕ n → vector ℕ m) :=
diff --git a/src/data/part.lean b/src/data/part.lean
index efc56b146ca41..d7162020a3362 100644
--- a/src/data/part.lean
+++ b/src/data/part.lean
@@ -484,4 +484,24 @@ theorem bind_defined {f : part α} {g : α → part β} :
 @[simp] theorem bind_dom {f : part α} {g : α → part β} :
   (f.bind g).dom ↔ ∃ h : f.dom, (g (f.get h)).dom := iff.rfl
 
+section instances
+
+/- We define several instances for constants and operations on `part α` inherited from `α`. -/
+
+instance [has_zero α] : has_zero (part α) := { zero := pure 0 }
+instance [has_one α] : has_one (part α) := { one := pure 1 }
+instance [has_add α] : has_add (part α) := { add := λ a b, (+) <$> a <*> b }
+instance [has_mul α] : has_mul (part α) := { mul := λ a b, (*) <$> a <*> b }
+instance [has_inv α] : has_inv (part α) := { inv := map has_inv.inv }
+instance [has_neg α] : has_neg (part α) := { neg := map has_neg.neg }
+instance [has_sub α] : has_sub (part α) := { sub := λ a b, (λ x y, x - y) <$> a <*> b }
+instance [has_div α] : has_div (part α) := { div := λ a b, (/) <$> a <*> b }
+instance [has_mod α] : has_mod (part α) := { mod := λ a b, (%) <$> a <*> b }
+instance [has_append α] : has_append (part α) := { append := λ a b, (++) <$> a <*> b }
+instance [has_inter α] : has_inter (part α) := { inter := λ a b, (∩) <$> a <*> b }
+instance [has_union α] : has_union (part α) := { union := λ a b, (∪) <$> a <*> b }
+instance [has_sdiff α] : has_sdiff (part α) := { sdiff := λ a b, (\) <$> a <*> b }
+
+end instances
+
 end part