diff --git a/src/computability/halting.lean b/src/computability/halting.lean
index 863fa43cf6889..96b598de66299 100644
--- a/src/computability/halting.lean
+++ b/src/computability/halting.lean
@@ -18,7 +18,7 @@ A universal partial recursive function, Rice's theorem, and the halting problem.
 open encodable denumerable
 
 namespace nat.partrec
-open computable roption
+open computable part
 
 theorem merge' {f g}
   (hf : nat.partrec f) (hg : nat.partrec g) :
@@ -60,7 +60,7 @@ namespace partrec
 variables {α : Type*} {β : Type*} {γ : Type*} {σ : Type*}
 variables [primcodable α] [primcodable β] [primcodable γ] [primcodable σ]
 
-open computable roption nat.partrec (code) nat.partrec.code
+open computable part nat.partrec (code) nat.partrec.code
 
 theorem merge' {f g : α →. σ}
   (hf : partrec f) (hg : partrec g) :
@@ -137,7 +137,7 @@ by exactI computable (λ a, to_bool (p a))
 /-- A recursively enumerable predicate is one which is the domain of a computable partial function.
  -/
 def re_pred {α} [primcodable α] (p : α → Prop) :=
-partrec (λ a, roption.assert (p a) (λ _, roption.some ()))
+partrec (λ a, part.assert (p a) (λ _, part.some ()))
 
 theorem computable_pred.of_eq {α} [primcodable α]
   {p q : α → Prop}
@@ -165,8 +165,8 @@ theorem to_re {p : α → Prop} (hp : computable_pred p) : re_pred p :=
 begin
   obtain ⟨f, hf, rfl⟩ := computable_iff.1 hp,
   unfold re_pred,
-  refine (partrec.cond hf (decidable.partrec.const' (roption.some ())) partrec.none).of_eq
-    (λ n, roption.ext $ λ a, _),
+  refine (partrec.cond hf (decidable.partrec.const' (part.some ())) partrec.none).of_eq
+    (λ n, part.ext $ λ a, _),
   cases a, cases f n; simp
 end
 
@@ -215,7 +215,7 @@ theorem computable_iff_re_compl_re {p : α → Prop} [decidable_pred p] :
   obtain ⟨k, pk, hk⟩ := partrec.merge
     (h₁.map (computable.const tt).to₂)
     (h₂.map (computable.const ff).to₂) _,
-  { refine partrec.of_eq pk (λ n, roption.eq_some_iff.2 _),
+  { refine partrec.of_eq pk (λ n, part.eq_some_iff.2 _),
     rw hk, simp, apply decidable.em },
   { intros a x hx y hy, simp at hx hy, cases hy.1 hx.1 }
 end⟩⟩
@@ -223,7 +223,7 @@ end⟩⟩
 end computable_pred
 
 namespace nat
-open vector roption
+open vector part
 
 /-- A simplified basis for `partrec`. -/
 inductive partrec' : ∀ {n}, (vector ℕ n →. ℕ) → Prop
@@ -247,7 +247,7 @@ begin
     exact (vector_m_of_fn (λ i, hg i)).bind (hf.comp snd) },
   case nat.partrec'.rfind : n f _ hf {
     have := ((primrec.eq.comp primrec.id (primrec.const 0)).to_comp.comp
-      (hf.comp (vector_cons.comp snd fst))).to₂.part,
+      (hf.comp (vector_cons.comp snd fst))).to₂.partrec₂,
     exact this.rfind },
 end
 
@@ -274,12 +274,12 @@ protected theorem bind {n f g}
     refine fin.cases _ (λ i, _) i; simp *,
     exact prim (nat.primrec'.nth _)
   end)).of_eq $
-λ v, by simp [m_of_fn, roption.bind_assoc, pure]
+λ v, by simp [m_of_fn, part.bind_assoc, pure]
 
 protected theorem map {n f} {g : vector ℕ (n+1) → ℕ}
   (hf : @partrec' n f) (hg : @partrec' (n+1) g) :
   @partrec' n (λ v, (f v).map (λ a, g (a ::ᵥ v))) :=
-by simp [(roption.bind_some_eq_map _ _).symm];
+by simp [(part.bind_some_eq_map _ _).symm];
    exact hf.bind hg
 
 /-- Analogous to `nat.partrec'` for `ℕ`-valued functions, a predicate for partial recursive
@@ -312,9 +312,9 @@ theorem rfind_opt {n} {f : vector ℕ (n+1) → ℕ}
   (hf : @partrec' (n+1) f) :
   @partrec' n (λ v, nat.rfind_opt (λ a, of_nat (option ℕ) (f (a ::ᵥ v)))) :=
 ((rfind $ (of_prim (primrec.nat_sub.comp (primrec.const 1) primrec.vector_head))
-   .comp₁ (λ n, roption.some (1 - n)) hf)
+   .comp₁ (λ n, part.some (1 - n)) hf)
    .bind ((prim nat.primrec'.pred).comp₁ nat.pred hf)).of_eq $
-λ v, roption.ext $ λ b, begin
+λ v, part.ext $ λ b, begin
   simp [nat.rfind_opt, -nat.mem_rfind],
   refine exists_congr (λ a,
     (and_congr (iff_of_eq _) iff.rfl).trans (and_congr_right (λ h, _))),
@@ -332,7 +332,7 @@ suffices ∀ f, nat.partrec f → @partrec' 1 (λ v, f v.head), from
 λ n f hf, begin
   let g, swap,
   exact (comp₁ g (this g hf) (prim nat.primrec'.encode)).of_eq
-    (λ i, by dsimp only [g]; simp [encodek, roption.map_id']),
+    (λ i, by dsimp only [g]; simp [encodek, part.map_id']),
 end,
 λ f hf, begin
   obtain ⟨c, rfl⟩ := exists_code.1 hf,
diff --git a/src/computability/partrec.lean b/src/computability/partrec.lean
index db8f468cf9447..538755d09a4fa 100644
--- a/src/computability/partrec.lean
+++ b/src/computability/partrec.lean
@@ -12,7 +12,7 @@ import data.pfun
 
 The partial recursive functions are defined similarly to the primitive
 recursive functions, but now all functions are partial, implemented
-using the `roption` monad, and there is an additional operation, called
+using the `part` monad, and there is an additional operation, called
 μ-recursion, which performs unbounded minimization.
 
 ## References
@@ -20,7 +20,7 @@ using the `roption` monad, and there is an additional operation, called
 * [Mario Carneiro, *Formalizing computability theory via partial recursive functions*][carneiro2019]
 -/
 
-open encodable denumerable roption
+open encodable denumerable part
 
 local attribute [-simp] not_forall
 
@@ -66,7 +66,7 @@ end
 
 end rfind
 
-def rfind (p : ℕ →. bool) : roption ℕ :=
+def rfind (p : ℕ →. bool) : part ℕ :=
 ⟨_, λ h, (rfind_x p h).1⟩
 
 theorem rfind_spec {p : ℕ →. bool} {n : ℕ} (h : n ∈ rfind p) : tt ∈ p n :=
@@ -110,9 +110,9 @@ theorem rfind_zero_none
   (p : ℕ →. bool) (p0 : p 0 = none) : rfind p = none :=
 eq_none_iff.2 $ λ a h,
 let ⟨n, h₁, h₂⟩ := rfind_dom'.1 h.fst in
-(p0 ▸ h₂ (zero_le _) : (@roption.none bool).dom)
+(p0 ▸ h₂ (zero_le _) : (@part.none bool).dom)
 
-def rfind_opt {α} (f : ℕ → option α) : roption α :=
+def rfind_opt {α} (f : ℕ → option α) : part α :=
 (rfind (λ n, (f n).is_some)).bind (λ n, f n)
 
 theorem rfind_opt_spec {α} {f : ℕ → option α} {a}
@@ -224,7 +224,7 @@ end nat
 
 def partrec {α σ} [primcodable α] [primcodable σ]
   (f : α →. σ) := nat.partrec (λ n,
-  roption.bind (decode α n) (λ a, (f a).map encode))
+  part.bind (decode α n) (λ a, (f a).map encode))
 
 def partrec₂ {α β σ} [primcodable α] [primcodable β] [primcodable σ]
   (f : α → β →. σ) := partrec (λ p : α × β, f p.1 p.2)
@@ -242,10 +242,10 @@ theorem primrec.to_comp {α σ} [primcodable α] [primcodable σ]
 theorem primrec₂.to_comp {α β σ} [primcodable α] [primcodable β] [primcodable σ]
   {f : α → β → σ} (hf : primrec₂ f) : computable₂ f := hf.to_comp
 
-theorem computable.part {α σ} [primcodable α] [primcodable σ]
+protected theorem computable.partrec {α σ} [primcodable α] [primcodable σ]
   {f : α → σ} (hf : computable f) : partrec (f : α →. σ) := hf
 
-theorem computable₂.part {α β σ} [primcodable α] [primcodable β] [primcodable σ]
+protected theorem computable₂.partrec₂ {α β σ} [primcodable α] [primcodable β] [primcodable σ]
   {f : α → β → σ} (hf : computable₂ f) : partrec₂ (λ a, (f a : β →. σ)) := hf
 
 namespace computable
@@ -258,8 +258,8 @@ theorem of_eq {f g : α → σ} (hf : computable f) (H : ∀ n, f n = g n) : com
 theorem const (s : σ) : computable (λ a : α, s) :=
 (primrec.const _).to_comp
 
-theorem of_option {f : α → option β}
-  (hf : computable f) : partrec (λ a, (f a : roption β)) :=
+theorem of_option {f : α → option β} (hf : computable f) :
+  partrec (λ a, (f a : part β)) :=
 (nat.partrec.ppred.comp hf).of_eq $ λ n, begin
   cases decode α n with a; simp,
   cases f a with b; simp
@@ -337,15 +337,15 @@ theorem of_eq_tot {f : α →. σ} {g : α → σ}
   (hf : partrec f) (H : ∀ n, g n ∈ f n) : computable g :=
 hf.of_eq (λ a, eq_some_iff.2 (H a))
 
-theorem none : partrec (λ a : α, @roption.none σ) :=
+theorem none : partrec (λ a : α, @part.none σ) :=
 nat.partrec.none.of_eq $ λ n, by cases decode α n; simp
 
-protected theorem some : partrec (@roption.some α) := computable.id
+protected theorem some : partrec (@part.some α) := computable.id
 
-theorem _root_.decidable.partrec.const' (s : roption σ) [decidable s.dom] : partrec (λ a : α, s) :=
+theorem _root_.decidable.partrec.const' (s : part σ) [decidable s.dom] : partrec (λ a : α, s) :=
 (of_option (const (to_option s))).of_eq (λ a, of_to_option s)
 
-theorem const' (s : roption σ) : partrec (λ a : α, s) :=
+theorem const' (s : part σ) : partrec (λ a : α, s) :=
 by haveI := classical.dec s.dom; exact decidable.partrec.const' s
 
 protected theorem bind {f : α →. β} {g : α → β →. σ}
@@ -357,7 +357,7 @@ protected theorem bind {f : α →. β} {g : α → β →. σ}
 theorem map {f : α →. β} {g : α → β → σ}
   (hf : partrec f) (hg : computable₂ g) : partrec (λ a, (f a).map (g a)) :=
 by simpa [bind_some_eq_map] using
-   @@partrec.bind _ _ _ (λ a b, roption.some (g a b)) hf hg
+   @@partrec.bind _ _ _ (λ a b, part.some (g a b)) hf hg
 
 theorem to₂ {f : α × β →. σ} (hf : partrec f) : partrec₂ (λ a b, f (a, b)) :=
 hf.of_eq $ λ ⟨a, b⟩, rfl
@@ -456,14 +456,14 @@ theorem rfind {p : α → ℕ →. bool} (hp : partrec₂ p) :
   cases e : decode α n with a;
     simp [e, nat.rfind_zero_none, map_id'],
   congr, funext n,
-  simp [roption.map_map, (∘)],
+  simp [part.map_map, (∘)],
   apply map_id' (λ b, _),
   cases b; refl
 end
 
 theorem rfind_opt {f : α → ℕ → option σ} (hf : computable₂ f) :
   partrec (λ a, nat.rfind_opt (f a)) :=
-(rfind (primrec.option_is_some.to_comp.comp hf).part.to₂).bind
+(rfind (primrec.option_is_some.to_comp.comp hf).partrec.to₂).bind
   (of_option hf)
 
 theorem nat_cases_right
@@ -475,14 +475,14 @@ theorem nat_cases_right
   simp, cases f a; simp,
   refine ext (λ b, ⟨λ H, _, λ H, _⟩),
   { rcases mem_bind_iff.1 H with ⟨c, h₁, h₂⟩, exact h₂ },
-  { have : ∀ m, (nat.elim (roption.some (g a))
+  { have : ∀ m, (nat.elim (part.some (g a))
       (λ y IH, IH.bind (λ _, h a n)) m).dom,
     { intro, induction m; simp [*, H.fst] },
     exact ⟨⟨this n, H.fst⟩, H.snd⟩ }
 end
 
 theorem bind_decode₂_iff {f : α →. σ} : partrec f ↔
-  nat.partrec (λ n, roption.bind (decode₂ α n) (λ a, (f a).map encode)) :=
+  nat.partrec (λ n, part.bind (decode₂ α n) (λ a, (f a).map encode)) :=
 ⟨λ hf, nat_iff.1 $ (of_option primrec.decode₂.to_comp).bind $
   (map hf (computable.encode.comp snd).to₂).comp snd,
 λ h, map_encode_iff.1 $ by simpa [encodek₂]
@@ -497,8 +497,8 @@ theorem vector_m_of_fn : ∀ {n} {f : fin n → α →. σ}, (∀ i, partrec (f
 
 end partrec
 
-@[simp] theorem vector.m_of_fn_roption_some {α n} : ∀ (f : fin n → α),
-  vector.m_of_fn (λ i, roption.some (f i)) = roption.some (vector.of_fn f) :=
+@[simp] theorem vector.m_of_fn_part_some {α n} : ∀ (f : fin n → α),
+  vector.m_of_fn (λ i, part.some (f i)) = part.some (vector.of_fn f) :=
 vector.m_of_fn_pure
 
 namespace computable
@@ -514,13 +514,13 @@ theorem bind_decode_iff {f : α → β → option σ} : computable₂ (λ a n,
 ⟨λ hf, nat.partrec.of_eq
     (((partrec.nat_iff.2 (nat.partrec.ppred.comp $
         nat.partrec.of_primrec $ primcodable.prim β)).comp snd).bind
-      (computable.comp hf fst).to₂.part) $
+      (computable.comp hf fst).to₂.partrec₂) $
   λ n, by simp;
     cases decode α n.unpair.1; simp;
     cases decode β n.unpair.2; simp,
 λ hf, begin
   have : partrec (λ a : α × ℕ, (encode (decode β a.2)).cases
-    (some option.none) (λ n, roption.map (f a.1) (decode β n))) :=
+    (some option.none) (λ n, part.map (f a.1) (decode β n))) :=
   partrec.nat_cases_right (primrec.encdec.to_comp.comp snd)
     (const none) ((of_option (computable.decode.comp snd)).map
       (hf.comp (fst.comp $ fst.comp fst) snd).to₂),
@@ -536,7 +536,7 @@ theorem nat_elim
   {f : α → ℕ} {g : α → σ} {h : α → ℕ × σ → σ}
   (hf : computable f) (hg : computable g) (hh : computable₂ h) :
   computable (λ a, (f a).elim (g a) (λ y IH, h a (y, IH))) :=
-(partrec.nat_elim hf hg hh.part).of_eq $
+(partrec.nat_elim hf hg hh.partrec₂).of_eq $
 λ a, by simp; induction f a; simp *
 
 theorem nat_cases {f : α → ℕ} {g : α → σ} {h : α → ℕ → σ}
@@ -629,15 +629,15 @@ open computable
 theorem option_some_iff {f : α →. σ} :
   partrec (λ a, (f a).map option.some) ↔ partrec f :=
 ⟨λ h, (nat.partrec.ppred.comp h).of_eq $
-   λ n, by simp [roption.bind_assoc, bind_some_eq_map],
+   λ n, by simp [part.bind_assoc, bind_some_eq_map],
  λ hf, hf.map (option_some.comp snd).to₂⟩
 
 theorem option_cases_right {o : α → option β} {f : α → σ} {g : α → β →. σ}
   (ho : computable o) (hf : computable f) (hg : partrec₂ g) :
   @partrec _ σ _ _ (λ a, option.cases_on (o a) (some (f a)) (g a)) :=
-have partrec (λ (a : α), nat.cases (roption.some (f a))
-  (λ n, roption.bind (decode β n) (g a)) (encode (o a))) :=
-nat_cases_right (encode_iff.2 ho) hf.part $
+have partrec (λ (a : α), nat.cases (part.some (f a))
+  (λ n, part.bind (decode β n) (g a)) (encode (o a))) :=
+nat_cases_right (encode_iff.2 ho) hf.partrec $
   ((@computable.decode β _).comp snd).of_option.bind
     (hg.comp (fst.comp fst) snd).to₂,
 this.of_eq $ λ a, by cases o a with b; simp [encodek]
@@ -649,7 +649,7 @@ have partrec (λ a, (option.cases_on
   (sum.cases_on (f a) (λ b, option.none) option.some : option γ)
   (some (sum.cases_on (f a) (λ b, some (g a b))
      (λ c, option.none)))
-  (λ c, (h a c).map option.some) : roption (option σ))) :=
+  (λ c, (h a c).map option.some) : part (option σ))) :=
 option_cases_right
   (sum_cases hf (const option.none).to₂ (option_some.comp snd).to₂)
   (sum_cases hf (option_some.comp hg) (const option.none).to₂)
@@ -666,7 +666,7 @@ theorem sum_cases_left {f : α → β ⊕ γ} {g : α → β →. σ} {h : α 
 lemma fix_aux {α σ} (f : α →. σ ⊕ α) (a : α) (b : σ) :
   let F : α → ℕ →. σ ⊕ α := λ a n,
     n.elim (some (sum.inr a)) $ λ y IH, IH.bind $ λ s,
-    sum.cases_on s (λ _, roption.some s) f in
+    sum.cases_on s (λ _, part.some s) f in
   (∃ (n : ℕ), ((∃ (b' : σ), sum.inl b' ∈ F a n) ∧
         ∀ {m : ℕ}, m < n → (∃ (b : α), sum.inr b ∈ F a m)) ∧
       sum.inl b ∈ F a n) ↔ b ∈ pfun.fix f a :=
@@ -707,13 +707,13 @@ end
 theorem fix {f : α →. σ ⊕ α} (hf : partrec f) : partrec (pfun.fix f) :=
 let F : α → ℕ →. σ ⊕ α := λ a n,
   n.elim (some (sum.inr a)) $ λ y IH, IH.bind $ λ s,
-  sum.cases_on s (λ _, roption.some s) f in
+  sum.cases_on s (λ _, part.some s) f in
 have hF : partrec₂ F :=
-partrec.nat_elim snd (sum_inr.comp fst).part
+partrec.nat_elim snd (sum_inr.comp fst).partrec
   (sum_cases_right (snd.comp snd)
     (snd.comp $ snd.comp fst).to₂
     (hf.comp snd).to₂).to₂,
-let p := λ a n, @roption.map _ bool
+let p := λ a n, @part.map _ bool
   (λ s, sum.cases_on s (λ_, tt) (λ _, ff)) (F a n) in
 have hp : partrec₂ p := hF.map ((sum_cases computable.id
   (const tt).to₂ (const ff).to₂).comp snd).to₂,
diff --git a/src/computability/partrec_code.lean b/src/computability/partrec_code.lean
index 9da8385ea9150..63bc302a87dba 100644
--- a/src/computability/partrec_code.lean
+++ b/src/computability/partrec_code.lean
@@ -494,11 +494,11 @@ def eval : code → ℕ →. ℕ
 
 instance : has_mem (ℕ →. ℕ) code := ⟨λ f c, eval c = f⟩
 
-@[simp] theorem eval_const : ∀ n m, eval (code.const n) m = roption.some n
+@[simp] theorem eval_const : ∀ n m, eval (code.const n) m = part.some n
 | 0     m := rfl
 | (n+1) m := by simp! *
 
-@[simp] theorem eval_id (n) : eval code.id n = roption.some n := by simp! [(<*>)]
+@[simp] theorem eval_id (n) : eval code.id n = part.some n := by simp! [(<*>)]
 
 @[simp] theorem eval_curry (c n x) : eval (curry c n) x = eval c (mkpair n x) :=
 by simp! [(<*>)]
@@ -541,7 +541,7 @@ theorem exists_code {f : ℕ →. ℕ} : nat.partrec f ↔ ∃ c : code, eval c
   case nat.partrec.rfind : f pf hf {
     rcases hf with ⟨cf, rfl⟩,
     refine ⟨comp (rfind' cf) (pair code.id zero), _⟩,
-    simp [eval, (<*>), pure, pfun.pure, roption.map_id'] },
+    simp [eval, (<*>), pure, pfun.pure, part.map_id'] },
 end, λ h, begin
   rcases h with ⟨c, rfl⟩, induction c,
   case nat.partrec.code.zero { exact nat.partrec.zero },
@@ -893,7 +893,7 @@ open partrec computable
 
 theorem eval_eq_rfind_opt (c n) :
   eval c n = nat.rfind_opt (λ k, evaln k c n) :=
-roption.ext $ λ x, begin
+part.ext $ λ x, begin
   refine evaln_complete.trans (nat.rfind_opt_mono _).symm,
   intros a m n hl, apply evaln_mono hl,
 end
@@ -905,30 +905,30 @@ theorem eval_part : partrec₂ eval :=
 
 theorem fixed_point
   {f : code → code} (hf : computable f) : ∃ c : code, eval (f c) = eval c :=
-let g (x y : ℕ) : roption ℕ :=
+let g (x y : ℕ) : part ℕ :=
   eval (of_nat code x) x >>= λ b, eval (of_nat code b) y in
 have partrec₂ g :=
   (eval_part.comp ((computable.of_nat _).comp fst) fst).bind
   (eval_part.comp ((computable.of_nat _).comp snd) (snd.comp fst)).to₂,
 let ⟨cg, eg⟩ := exists_code.1 this in
-have eg' : ∀ a n, eval cg (mkpair a n) = roption.map encode (g a n) :=
+have eg' : ∀ a n, eval cg (mkpair a n) = part.map encode (g a n) :=
   by simp [eg],
 let F (x : ℕ) : code := f (curry cg x) in
 have computable F :=
   hf.comp (curry_prim.comp (primrec.const cg) primrec.id).to_comp,
 let ⟨cF, eF⟩ := exists_code.1 this in
-have eF' : eval cF (encode cF) = roption.some (encode (F (encode cF))),
+have eF' : eval cF (encode cF) = part.some (encode (F (encode cF))),
   by simp [eF],
 ⟨curry cg (encode cF), funext (λ n,
   show eval (f (curry cg (encode cF))) n = eval (curry cg (encode cF)) n,
-  by simp [eg', eF', roption.map_id', g])⟩
+  by simp [eg', eF', part.map_id', g])⟩
 
 theorem fixed_point₂
   {f : code → ℕ →. ℕ} (hf : partrec₂ f) : ∃ c : code, eval c = f c :=
 let ⟨cf, ef⟩ := exists_code.1 hf in
 (fixed_point (curry_prim.comp
   (primrec.const cf) primrec.encode).to_comp).imp $
-λ c e, funext $ λ n, by simp [e.symm, ef, roption.map_id']
+λ c e, funext $ λ n, by simp [e.symm, ef, part.map_id']
 
 end
 
diff --git a/src/computability/tm_to_partrec.lean b/src/computability/tm_to_partrec.lean
index 3ea2adca013c1..4c67003579f9d 100644
--- a/src/computability/tm_to_partrec.lean
+++ b/src/computability/tm_to_partrec.lean
@@ -178,7 +178,7 @@ let G := cons tail $ cons succ $ cons (comp pred tail) $
 let F := case id $ comp (comp (comp tail tail) (fix G)) zero' in
 cons (comp F (cons head $ cons (comp f tail) tail)) nil
 
-local attribute [-simp] roption.bind_eq_bind roption.map_eq_map roption.pure_eq_some
+local attribute [-simp] part.bind_eq_bind part.map_eq_map part.pure_eq_some
 
 theorem exists_code.comp {m n} {f : vector ℕ n →. ℕ} {g : fin n → vector ℕ m →. ℕ}
   (hf : ∃ c : code, ∀ v : vector ℕ n, c.eval v.1 = pure <$> f v)
@@ -210,17 +210,17 @@ begin
     { obtain ⟨c, h⟩ := IH,
       exact ⟨c.comp tail, λ v, by simpa [← vector.nth_tail] using h v.tail⟩ } },
   case prim comp : m n f g hf hg IHf IHg {
-    simpa [roption.bind_eq_bind] using exists_code.comp IHf IHg },
+    simpa [part.bind_eq_bind] using exists_code.comp IHf IHg },
   case prim prec : n f g hf hg IHf IHg {
     obtain ⟨cf, hf⟩ := IHf, obtain ⟨cg, hg⟩ := IHg,
-    simp only [roption.map_eq_map, roption.map_some, pfun.coe_val] at hf hg,
+    simp only [part.map_eq_map, part.map_some, pfun.coe_val] at hf hg,
     refine ⟨prec cf cg, λ v, _⟩, rw ← v.cons_head_tail,
     specialize hf v.tail, replace hg := λ a b, hg (a ::ᵥ b ::ᵥ v.tail),
     simp only [vector.cons_val, vector.tail_val] at hf hg,
-    simp only [roption.map_eq_map, roption.map_some, vector.cons_val,
+    simp only [part.map_eq_map, part.map_some, vector.cons_val,
       vector.cons_tail, vector.cons_head, pfun.coe_val, vector.tail_val],
-    simp only [← roption.pure_eq_some] at hf hg ⊢,
-    induction v.head with n IH; simp [prec, hf, bind_assoc, ← roption.map_eq_map,
+    simp only [← part.pure_eq_some] at hf hg ⊢,
+    induction v.head with n IH; simp [prec, hf, bind_assoc, ← part.map_eq_map,
       ← bind_pure_comp_eq_map, show ∀ x, pure x = [x], from λ _, rfl, -subtype.val_eq_coe],
     suffices : ∀ a b, a + b = n →
       (n.succ :: 0 :: g
@@ -233,30 +233,30 @@ begin
           else sum.inr (v.head.succ :: v.tail.head.pred :: x.head :: v.tail.tail.tail))
         (a :: b :: nat.elim (f v.tail)
           (λ y IH, g (y ::ᵥ IH ::ᵥ v.tail)) a :: v.val.tail),
-    { rw (_ : pfun.fix _ _ = pure _), swap, exact roption.eq_some_iff.2 (this 0 n (zero_add n)),
+    { rw (_ : pfun.fix _ _ = pure _), swap, exact part.eq_some_iff.2 (this 0 n (zero_add n)),
       simp only [list.head, pure_bind, list.tail_cons] },
     intros a b e, induction b with b IH generalizing a e,
-    { refine pfun.mem_fix_iff.2 (or.inl $ roption.eq_some_iff.1 _),
+    { refine pfun.mem_fix_iff.2 (or.inl $ part.eq_some_iff.1 _),
       simp only [hg, ← e, pure_bind, list.tail_cons], refl },
     { refine pfun.mem_fix_iff.2 (or.inr ⟨_, _, IH (a+1) (by rwa add_right_comm)⟩),
       simp only [hg, eval, pure_bind, nat.elim_succ, list.tail],
-      exact roption.mem_some_iff.2 rfl } },
+      exact part.mem_some_iff.2 rfl } },
   case comp : m n f g hf hg IHf IHg { exact exists_code.comp IHf IHg },
   case rfind : n f hf IHf {
     obtain ⟨cf, hf⟩ := IHf, refine ⟨rfind cf, λ v, _⟩,
     replace hf := λ a, hf (a ::ᵥ v),
-    simp only [roption.map_eq_map, roption.map_some, vector.cons_val, pfun.coe_val,
+    simp only [part.map_eq_map, part.map_some, vector.cons_val, pfun.coe_val,
       show ∀ x, pure x = [x], from λ _, rfl] at hf ⊢,
-    refine roption.ext (λ x, _),
-    simp only [rfind, roption.bind_eq_bind, roption.pure_eq_some, roption.map_eq_map,
-      roption.bind_some, exists_prop, eval, list.head, pred_eval, roption.map_some,
-      bool.ff_eq_to_bool_iff, roption.mem_bind_iff, list.length,
-      roption.mem_map_iff, nat.mem_rfind, list.tail, bool.tt_eq_to_bool_iff,
-      roption.mem_some_iff, roption.map_bind],
+    refine part.ext (λ x, _),
+    simp only [rfind, part.bind_eq_bind, part.pure_eq_some, part.map_eq_map,
+      part.bind_some, exists_prop, eval, list.head, pred_eval, part.map_some,
+      bool.ff_eq_to_bool_iff, part.mem_bind_iff, list.length,
+      part.mem_map_iff, nat.mem_rfind, list.tail, bool.tt_eq_to_bool_iff,
+      part.mem_some_iff, part.map_bind],
     split,
     { rintro ⟨v', h1, rfl⟩,
       suffices : ∀ (v₁ : list ℕ), v' ∈ pfun.fix
-        (λ v, (cf.eval v).bind $ λ y, roption.some $ if y.head = 0 then
+        (λ v, (cf.eval v).bind $ λ y, part.some $ if y.head = 0 then
           sum.inl (v.head.succ :: v.tail) else sum.inr (v.head.succ :: v.tail)) v₁ →
         ∀ n, v₁ = n :: v.val → (∀ m < n, ¬f (m ::ᵥ v) = 0) →
         (∃ (a : ℕ), (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧
@@ -266,25 +266,25 @@ begin
       refine pfun.fix_induction h1 (λ v₁ h2 IH, _), clear h1,
       rintro n rfl hm,
       have := pfun.mem_fix_iff.1 h2,
-      simp only [hf, roption.bind_some] at this,
+      simp only [hf, part.bind_some] at this,
       split_ifs at this,
-      { simp only [list.head, exists_false, or_false, roption.mem_some_iff,
+      { simp only [list.head, exists_false, or_false, part.mem_some_iff,
           list.tail_cons, false_and] at this,
         subst this, exact ⟨_, ⟨h, hm⟩, rfl⟩ },
-      { simp only [list.head, exists_eq_left, roption.mem_some_iff,
+      { simp only [list.head, exists_eq_left, part.mem_some_iff,
           list.tail_cons, false_or] at this,
         refine IH _ this (by simp [hf, h, -subtype.val_eq_coe]) _ rfl (λ m h', _),
         obtain h|rfl := nat.lt_succ_iff_lt_or_eq.1 h', exacts [hm _ h, h] } },
     { rintro ⟨n, ⟨hn, hm⟩, rfl⟩, refine ⟨n.succ :: v.1, _, rfl⟩,
       have : (n.succ :: v.1 : list ℕ) ∈ pfun.fix
-        (λ v, (cf.eval v).bind $ λ y, roption.some $ if y.head = 0 then
+        (λ v, (cf.eval v).bind $ λ y, part.some $ if y.head = 0 then
           sum.inl (v.head.succ :: v.tail) else sum.inr (v.head.succ :: v.tail)) (n :: v.val) :=
         pfun.mem_fix_iff.2 (or.inl (by simp [hf, hn, -subtype.val_eq_coe])),
       generalize_hyp : (n.succ :: v.1 : list ℕ) = w at this ⊢, clear hn,
       induction n with n IH, {exact this},
       refine IH (λ m h', hm (nat.lt_succ_of_lt h')) (pfun.mem_fix_iff.2 (or.inr ⟨_, _, this⟩)),
-      simp only [hf, hm n.lt_succ_self, roption.bind_some, list.head, eq_self_iff_true,
-        if_false, roption.mem_some_iff, and_self, list.tail_cons] } }
+      simp only [hf, hm n.lt_succ_self, part.bind_some, list.head, eq_self_iff_true,
+        if_false, part.mem_some_iff, and_self, list.tail_cons] } }
 end
 
 end code
@@ -479,7 +479,7 @@ theorem code.ok.zero {c} (h : code.ok c) {v} :
   eval step (step_normal c cont.halt v) = cfg.halt <$> code.eval c v :=
 begin
   rw [h, ← bind_pure_comp_eq_map], congr, funext v,
-  exact roption.eq_some_iff.2 (mem_eval.2 ⟨refl_trans_gen.single rfl, rfl⟩),
+  exact part.eq_some_iff.2 (mem_eval.2 ⟨refl_trans_gen.single rfl, rfl⟩),
 end
 
 theorem step_normal.is_ret (c k v) : ∃ k' v', step_normal c k v = cfg.ret k' v' :=
@@ -496,8 +496,8 @@ end
 theorem cont_eval_fix {f k v} (fok : code.ok f) :
   eval step (step_normal f (cont.fix f k) v) = f.fix.eval v >>= λ v, eval step (cfg.ret k v) :=
 begin
-  refine roption.ext (λ x, _),
-  simp only [roption.bind_eq_bind, roption.mem_bind_iff],
+  refine part.ext (λ x, _),
+  simp only [part.bind_eq_bind, part.mem_bind_iff],
   split,
   { suffices :
       ∀ c, x ∈ eval step c →
@@ -509,20 +509,20 @@ begin
       obtain ⟨v₁, hv₁, v₂, hv₂, h₃⟩ :=
         this _ h _ _ (step_normal_then _ cont.halt _ _) refl_trans_gen.refl,
       refine ⟨v₂, pfun.mem_fix_iff.2 _, h₃⟩,
-      simp only [roption.eq_some_iff.2 hv₁, roption.map_some],
+      simp only [part.eq_some_iff.2 hv₁, part.map_some],
       split_ifs at hv₂ ⊢,
-      { rw roption.mem_some_iff.1 hv₂, exact or.inl (roption.mem_some _) },
-      { exact or.inr ⟨_, roption.mem_some _, hv₂⟩ } },
+      { rw part.mem_some_iff.1 hv₂, exact or.inl (part.mem_some _) },
+      { exact or.inr ⟨_, part.mem_some _, hv₂⟩ } },
     refine λ c he, eval_induction he (λ y h IH, _),
     rintro v (⟨v'⟩ | ⟨k',v'⟩) rfl hr; rw cfg.then at h IH,
     { have := mem_eval.2 ⟨hr, rfl⟩,
-      rw [fok, roption.bind_eq_bind, roption.mem_bind_iff] at this,
+      rw [fok, part.bind_eq_bind, part.mem_bind_iff] at this,
       obtain ⟨v'', h₁, h₂⟩ := this,
       rw reaches_eval at h₂, swap, exact refl_trans_gen.single rfl,
-      cases roption.mem_unique h₂ (mem_eval.2 ⟨refl_trans_gen.refl, rfl⟩),
+      cases part.mem_unique h₂ (mem_eval.2 ⟨refl_trans_gen.refl, rfl⟩),
       refine ⟨v', h₁, _⟩, rw [step_ret] at h,
       revert h, by_cases he : v'.head = 0; simp only [exists_prop, if_pos, if_false, he]; intro h,
-      { refine ⟨_, roption.mem_some _, _⟩,
+      { refine ⟨_, part.mem_some _, _⟩,
         rw reaches_eval, exact h, exact refl_trans_gen.single rfl },
       { obtain ⟨k₀, v₀, e₀⟩ := step_normal.is_ret f cont.halt v'.tail,
         have e₁ := step_normal_then f cont.halt (cont.fix f k) v'.tail,
@@ -530,8 +530,8 @@ begin
         obtain ⟨v₁, hv₁, v₂, hv₂, h₃⟩ :=
           IH (step_ret (k₀.then (cont.fix f k)) v₀) _ _ v'.tail _ step_ret_then _,
         { refine ⟨_, pfun.mem_fix_iff.2 _, h₃⟩,
-          simp only [roption.eq_some_iff.2 hv₁, roption.map_some, roption.mem_some_iff],
-          split_ifs at hv₂ ⊢; [exact or.inl (roption.mem_some_iff.1 hv₂),
+          simp only [part.eq_some_iff.2 hv₁, part.map_some, part.mem_some_iff],
+          split_ifs at hv₂ ⊢; [exact or.inl (part.mem_some_iff.1 hv₂),
             exact or.inr ⟨_, rfl, hv₂⟩] },
         { rwa [← @reaches_eval _ _ (cfg.ret (k₀.then (cont.fix f k)) v₀), ← e₁],
           exact refl_trans_gen.single rfl },
@@ -542,18 +542,18 @@ begin
   { rintro ⟨v', he, hr⟩,
     rw reaches_eval at hr, swap, exact refl_trans_gen.single rfl,
     refine pfun.fix_induction he (λ v (he : v' ∈ f.fix.eval v) IH, _),
-    rw [fok, roption.bind_eq_bind, roption.mem_bind_iff],
+    rw [fok, part.bind_eq_bind, part.mem_bind_iff],
     obtain he | ⟨v'', he₁', he₂'⟩ := pfun.mem_fix_iff.1 he,
-    { obtain ⟨v', he₁, he₂⟩ := (roption.mem_map_iff _).1 he, split_ifs at he₂; cases he₂,
+    { obtain ⟨v', he₁, he₂⟩ := (part.mem_map_iff _).1 he, split_ifs at he₂; cases he₂,
       refine ⟨_, he₁, _⟩,
       rw reaches_eval, swap, exact refl_trans_gen.single rfl,
       rwa [step_ret, if_pos h] },
-    { obtain ⟨v₁, he₁, he₂⟩ := (roption.mem_map_iff _).1 he₁', split_ifs at he₂; cases he₂,
+    { obtain ⟨v₁, he₁, he₂⟩ := (part.mem_map_iff _).1 he₁', split_ifs at he₂; cases he₂,
       clear he₂ he₁', change _ ∈ f.fix.eval _ at he₂',
       refine ⟨_, he₁, _⟩,
       rw reaches_eval, swap, exact refl_trans_gen.single rfl,
       rwa [step_ret, if_neg h],
-      exact IH v₁.tail he₂' ((roption.mem_map_iff _).2 ⟨_, he₁, if_neg h⟩) } }
+      exact IH v₁.tail he₂' ((part.mem_map_iff _).2 ⟨_, he₁, if_neg h⟩) } }
 end
 
 theorem code_is_ok (c) : code.ok c :=
@@ -586,7 +586,7 @@ begin
   induction k generalizing v,
   case halt : {
     simp only [mem_eval, cont.eval, map_pure],
-    exact roption.eq_some_iff.2 (mem_eval.2 ⟨refl_trans_gen.refl, rfl⟩) },
+    exact part.eq_some_iff.2 (mem_eval.2 ⟨refl_trans_gen.refl, rfl⟩) },
   case cons₁ : fs as k IH {
     rw [cont.eval, step_ret, code_is_ok],
     simp only [← bind_pure_comp_eq_map, bind_assoc], congr, funext v',
@@ -1304,7 +1304,7 @@ theorem tr_init (c v) : ∃ b, tr_cfg (step_normal c cont.halt v) b ∧
 theorem tr_eval (c v) : eval (TM2.step tr) (init c v) = halt <$> code.eval c v :=
 begin
   obtain ⟨i, h₁, h₂⟩ := tr_init c v,
-  refine roption.ext (λ x, _),
+  refine part.ext (λ x, _),
   rw [reaches_eval h₂.to_refl], simp,
   refine ⟨λ h, _, _⟩,
   { obtain ⟨c, hc₁, hc₂⟩ := tr_eval_rev tr_respects h₁ h,
diff --git a/src/computability/turing_machine.lean b/src/computability/turing_machine.lean
index 41921f89a6afc..18da3edca369a 100644
--- a/src/computability/turing_machine.lean
+++ b/src/computability/turing_machine.lean
@@ -44,7 +44,7 @@ Given these parameters, there are a few common structures for the model that ari
   from `c`. Because of the type of `step`, these models are all deterministic by construction.
 * `init : input → cfg` sets up the initial state. The type `input` depends on the model;
   in most cases it is `list Γ`.
-* `eval : machine → input → roption output`, given a machine `M` and input `i`, starts from
+* `eval : machine → input → part output`, given a machine `M` and input `i`, starts from
   `init i`, runs `step` until it reaches an output, and then applies a function `cfg → output` to
   the final state to obtain the result. The type `output` depends on the model.
 * `supports : machine → finset Λ → Prop` asserts that a machine `M` starts in `S : finset Λ`, and
@@ -584,9 +584,9 @@ theorem tape.map_mk₁ {Γ Γ'} [inhabited Γ] [inhabited Γ'] (f : pointed_map
 
 /-- Run a state transition function `σ → option σ` "to completion". The return value is the last
 state returned before a `none` result. If the state transition function always returns `some`,
-then the computation diverges, returning `roption.none`. -/
-def eval {σ} (f : σ → option σ) : σ → roption σ :=
-pfun.fix (λ s, roption.some $ (f s).elim (sum.inl s) sum.inr)
+then the computation diverges, returning `part.none`. -/
+def eval {σ} (f : σ → option σ) : σ → part σ :=
+pfun.fix (λ s, part.some $ (f s).elim (sum.inl s) sum.inr)
 
 /-- The reflexive transitive closure of a state transition function. `reaches f a b` means
 there is a finite sequence of steps `f a = some a₁`, `f a₁ = some a₂`, ... such that `aₙ = b`.
@@ -666,27 +666,27 @@ holds of any point where `eval f a` evaluates to `b`. This formalizes the notion
   (H : ∀ a, b ∈ eval f a →
     (∀ a', b ∈ eval f a' → f a = some a' → C a') → C a) : C a :=
 pfun.fix_induction h (λ a' ha' h', H _ ha' $ λ b' hb' e, h' _ hb' $
-  roption.mem_some_iff.2 $ by rw e; refl)
+  part.mem_some_iff.2 $ by rw e; refl)
 
 theorem mem_eval {σ} {f : σ → option σ} {a b} :
   b ∈ eval f a ↔ reaches f a b ∧ f b = none :=
 ⟨λ h, begin
   refine eval_induction h (λ a h IH, _),
   cases e : f a with a',
-  { rw roption.mem_unique h (pfun.mem_fix_iff.2 $ or.inl $
-      roption.mem_some_iff.2 $ by rw e; refl),
+  { rw part.mem_unique h (pfun.mem_fix_iff.2 $ or.inl $
+      part.mem_some_iff.2 $ by rw e; refl),
     exact ⟨refl_trans_gen.refl, e⟩ },
   { rcases pfun.mem_fix_iff.1 h with h | ⟨_, h, h'⟩;
-      rw e at h; cases roption.mem_some_iff.1 h,
+      rw e at h; cases part.mem_some_iff.1 h,
     cases IH a' h' (by rwa e) with h₁ h₂,
     exact ⟨refl_trans_gen.head e h₁, h₂⟩ }
 end, λ ⟨h₁, h₂⟩, begin
   refine refl_trans_gen.head_induction_on h₁ _ (λ a a' h _ IH, _),
   { refine pfun.mem_fix_iff.2 (or.inl _),
-    rw h₂, apply roption.mem_some },
+    rw h₂, apply part.mem_some },
   { refine pfun.mem_fix_iff.2 (or.inr ⟨_, _, IH⟩),
     rw show f a = _, from h,
-    apply roption.mem_some }
+    apply part.mem_some }
 end⟩
 
 theorem eval_maximal₁ {σ} {f : σ → option σ} {a b}
@@ -701,7 +701,7 @@ refl_trans_gen_iff_eq $ λ b' h', by cases b0.symm.trans h'
 
 theorem reaches_eval {σ} {f : σ → option σ} {a b}
   (ab : reaches f a b) : eval f a = eval f b :=
-roption.ext $ λ c,
+part.ext $ λ c,
  ⟨λ h, let ⟨ac, c0⟩ := mem_eval.1 h in
     mem_eval.2 ⟨(or_iff_left_of_imp $ by exact
       λ cb, (eval_maximal h).1 cb ▸ refl_trans_gen.refl).1
@@ -812,11 +812,11 @@ theorem tr_eval' {σ₁ σ₂}
   (f₁ : σ₁ → option σ₁) (f₂ : σ₂ → option σ₂) (tr : σ₁ → σ₂)
   (H : respects f₁ f₂ (λ a b, tr a = b))
   (a₁) : eval f₂ (tr a₁) = tr <$> eval f₁ a₁ :=
-roption.ext $ λ b₂,
+part.ext $ λ b₂,
  ⟨λ h, let ⟨b₁, bb, hb⟩ := tr_eval_rev H rfl h in
-    (roption.mem_map_iff _).2 ⟨b₁, hb, bb⟩,
+    (part.mem_map_iff _).2 ⟨b₁, hb, bb⟩,
   λ h, begin
-    rcases (roption.mem_map_iff _).1 h with ⟨b₁, ab, bb⟩,
+    rcases (part.mem_map_iff _).1 h with ⟨b₁, ab, bb⟩,
     rcases tr_eval H rfl ab with ⟨_, rfl, h⟩,
     rwa bb at h
   end⟩
@@ -904,7 +904,7 @@ def init (l : list Γ) : cfg :=
 
 /-- Evaluate a Turing machine on initial input to a final state,
   if it terminates. -/
-def eval (M : machine) (l : list Γ) : roption (list_blank Γ) :=
+def eval (M : machine) (l : list Γ) : part (list_blank Γ) :=
 (eval (step M) (init l)).map (λ c, c.tape.right₀)
 
 /-- The raw definition of a Turing machine does not require that
@@ -1183,7 +1183,7 @@ def init (l : list Γ) : cfg :=
 
 /-- Evaluate a TM to completion, resulting in an output list on the tape (with an indeterminate
 number of blanks on the end). -/
-def eval (M : Λ → stmt) (l : list Γ) : roption (list_blank Γ) :=
+def eval (M : Λ → stmt) (l : list Γ) : part (list_blank Γ) :=
 (eval (step M) (init l)).map (λ c, c.tape.right₀)
 
 end
@@ -1278,7 +1278,7 @@ end
 
 theorem tr_eval (l : list Γ) : TM0.eval tr l = TM1.eval M l :=
 (congr_arg _ (tr_eval' _ _ _ tr_respects ⟨some _, _, _⟩)).trans begin
-  rw [roption.map_eq_map, roption.map_map, TM1.eval],
+  rw [part.map_eq_map, part.map_map, TM1.eval],
   congr' with ⟨⟩, refl
 end
 
@@ -1951,7 +1951,7 @@ def init (k) (L : list (Γ k)) : cfg :=
 ⟨some (default _), default _, update (λ _, []) k L⟩
 
 /-- Evaluates a TM2 program to completion, with the output on the same stack as the input. -/
-def eval (M : Λ → stmt) (k) (L : list (Γ k)) : roption (list (Γ k)) :=
+def eval (M : Λ → stmt) (k) (L : list (Γ k)) : part (list (Γ k)) :=
 (eval (step M) (init k L)).map $ λ c, c.stk k
 
 end
@@ -2380,10 +2380,10 @@ theorem tr_eval (k) (L : list (Γ k)) {L₁ L₂}
     (∀ k, L'.map (proj k) = list_blank.mk ((S k).map some).reverse) ∧
     S k = L₂ :=
 begin
-  obtain ⟨c₁, h₁, rfl⟩ := (roption.mem_map_iff _).1 H₁,
-  obtain ⟨c₂, h₂, rfl⟩ := (roption.mem_map_iff _).1 H₂,
+  obtain ⟨c₁, h₁, rfl⟩ := (part.mem_map_iff _).1 H₁,
+  obtain ⟨c₂, h₂, rfl⟩ := (part.mem_map_iff _).1 H₂,
   obtain ⟨_, ⟨q, v, S, L', hT⟩, h₃⟩ := tr_eval (tr_respects M) (tr_cfg_init M k L) h₂,
-  cases roption.mem_unique h₁ h₃,
+  cases part.mem_unique h₁ h₃,
   exact ⟨S, L', by simp only [tape.mk'_right₀], hT, rfl⟩
 end
 
diff --git a/src/control/fix.lean b/src/control/fix.lean
index cc257a5177d54..6342d1d3b4920 100644
--- a/src/control/fix.lean
+++ b/src/control/fix.lean
@@ -13,12 +13,12 @@ import data.pfun
 
 This module defines a generic `fix` operator for defining recursive
 computations that are not necessarily well-founded or productive.
-An instance is defined for `roption`.
+An instance is defined for `part`.
 
 ## Main definition
 
  * class `has_fix`
- * `roption.fix`
+ * `part.fix`
 -/
 
 universes u v
@@ -31,23 +31,23 @@ of function of type `α → α`. -/
 class has_fix (α : Type*) :=
 (fix : (α → α) → α)
 
-namespace roption
+namespace part
 
-open roption nat nat.upto
+open part nat nat.upto
 
 section basic
 
-variables (f : (Π a, roption $ β a) → (Π a, roption $ β a))
+variables (f : (Π a, part $ β a) → (Π a, part $ β a))
 
 /-- A series of successive, finite approximation of the fixed point of `f`, defined by
 `approx f n = f^[n] ⊥`. The limit of this chain is the fixed point of `f`. -/
-def fix.approx : stream $ Π a, roption $ β a
+def fix.approx : stream $ Π a, part $ β a
 | 0 := ⊥
 | (nat.succ i) := f (fix.approx i)
 
 /-- loop body for finding the fixed point of `f` -/
 def fix_aux {p : ℕ → Prop} (i : nat.upto p)
-  (g : Π j : nat.upto p, i < j → Π a, roption $ β a) : Π a, roption $ β a :=
+  (g : Π j : nat.upto p, i < j → Π a, part $ β a) : Π a, part $ β a :=
 f $ λ x : α,
 assert (¬p (i.val)) $ λ h : ¬ p (i.val),
 g (i.succ h) (nat.lt_succ_self _) x
@@ -60,12 +60,12 @@ it satisfies the equations:
   1. `fix f = f (fix f)`          (is a fixed point)
   2. `∀ X, f X ≤ X → fix f ≤ X`   (least fixed point)
 -/
-protected def fix (x : α) : roption $ β x :=
-roption.assert (∃ i, (fix.approx f i x).dom) $ λ h,
+protected def fix (x : α) : part $ β x :=
+part.assert (∃ i, (fix.approx f i x).dom) $ λ h,
 well_founded.fix.{1} (nat.upto.wf h) (fix_aux f) nat.upto.zero x
 
 protected lemma fix_def {x : α} (h' : ∃ i, (fix.approx f i x).dom) :
-  roption.fix f x = fix.approx f (nat.succ $ nat.find h') x :=
+  part.fix f x = fix.approx f (nat.succ $ nat.find h') x :=
 begin
   let p := λ (i : ℕ), (fix.approx f i x).dom,
   have : p (nat.find h') := nat.find_spec h',
@@ -73,7 +73,7 @@ begin
   replace hk : nat.find h' = k + (@upto.zero p).val := hk,
   rw hk at this,
   revert hk,
-  dsimp [roption.fix], rw assert_pos h', revert this,
+  dsimp [part.fix], rw assert_pos h', revert this,
   generalize : upto.zero = z, intros,
   suffices : ∀ x',
     well_founded.fix (fix._proof_1 f x h') (fix_aux f) z x' = fix.approx f (succ k) x',
@@ -95,24 +95,24 @@ begin
 end
 
 lemma fix_def' {x : α} (h' : ¬ ∃ i, (fix.approx f i x).dom) :
-  roption.fix f x = none :=
-by dsimp [roption.fix]; rw assert_neg h'
+  part.fix f x = none :=
+by dsimp [part.fix]; rw assert_neg h'
 
 end basic
 
-end roption
+end part
 
-namespace roption
+namespace part
 
-instance : has_fix (roption α) :=
-⟨λ f, roption.fix (λ x u, f (x u)) ()⟩
+instance : has_fix (part α) :=
+⟨λ f, part.fix (λ x u, f (x u)) ()⟩
 
-end roption
+end part
 
 open sigma
 
 namespace pi
 
-instance roption.has_fix {β} : has_fix (α → roption β) := ⟨roption.fix⟩
+instance part.has_fix {β} : has_fix (α → part β) := ⟨part.fix⟩
 
 end pi
diff --git a/src/control/lawful_fix.lean b/src/control/lawful_fix.lean
index 72cb7dab4d130..4548dede4a885 100644
--- a/src/control/lawful_fix.lean
+++ b/src/control/lawful_fix.lean
@@ -41,13 +41,13 @@ lemma lawful_fix.fix_eq' {α} [omega_complete_partial_order α] [lawful_fix α]
   has_fix.fix f = f (has_fix.fix f) :=
 lawful_fix.fix_eq (continuous.to_bundled _ hf)
 
-namespace roption
+namespace part
 
-open roption nat nat.upto
+open part nat nat.upto
 
 namespace fix
 
-variables (f : (Π a, roption $ β a) →ₘ (Π a, roption $ β a))
+variables (f : (Π a, part $ β a) →ₘ (Π a, part $ β a))
 
 lemma approx_mono' {i : ℕ} : fix.approx f i ≤ fix.approx f (succ i) :=
 begin
@@ -63,10 +63,10 @@ begin
   apply approx_mono' f
 end
 
-lemma mem_iff (a : α) (b : β a) : b ∈ roption.fix f a ↔ ∃ i, b ∈ approx f i a :=
+lemma mem_iff (a : α) (b : β a) : b ∈ part.fix f a ↔ ∃ i, b ∈ approx f i a :=
 begin
   by_cases h₀ : ∃ (i : ℕ), (approx f i a).dom,
-  { simp only [roption.fix_def f h₀],
+  { simp only [part.fix_def f h₀],
     split; intro hh, exact ⟨_,hh⟩,
     have h₁ := nat.find_spec h₀,
     rw [dom_iff_mem] at h₁,
@@ -77,23 +77,23 @@ begin
     revert h₁, generalize : (succ (nat.find h₀)) = j, intro,
     wlog : i ≤ j := le_total i j using [i j b y,j i y b],
     replace hh := approx_mono f case _ _ hh,
-    apply roption.mem_unique h₁ hh },
+    apply part.mem_unique h₁ hh },
   { simp only [fix_def' ⇑f h₀, not_exists, false_iff, not_mem_none],
     simp only [dom_iff_mem, not_exists] at h₀,
     intro, apply h₀ }
 end
 
-lemma approx_le_fix (i : ℕ) : approx f i ≤ roption.fix f :=
+lemma approx_le_fix (i : ℕ) : approx f i ≤ part.fix f :=
 assume a b hh,
 by { rw [mem_iff f], exact ⟨_,hh⟩ }
 
-lemma exists_fix_le_approx (x : α) : ∃ i, roption.fix f x ≤ approx f i x :=
+lemma exists_fix_le_approx (x : α) : ∃ i, part.fix f x ≤ approx f i x :=
 begin
   by_cases hh : ∃ i b, b ∈ approx f i x,
   { rcases hh with ⟨i,b,hb⟩, existsi i,
     intros b' h',
     have hb' := approx_le_fix f i _ _ hb,
-    have hh := roption.mem_unique h' hb',
+    have hh := part.mem_unique h' hb',
     subst hh, exact hb },
   { simp only [not_exists] at hh, existsi 0,
     intros b' h',
@@ -105,7 +105,7 @@ end
 include f
 
 /-- The series of approximations of `fix f` (see `approx`) as a `chain` -/
-def approx_chain : chain (Π a, roption $ β a) := ⟨approx f, approx_mono f⟩
+def approx_chain : chain (Π a, part $ β a) := ⟨approx f, approx_mono f⟩
 
 lemma le_f_of_mem_approx {x} (hx : x ∈ approx_chain f) : x ≤ f x :=
 begin
@@ -122,14 +122,14 @@ end fix
 open fix
 
 variables {α}
-variables (f : (Π a, roption $ β a) →ₘ (Π a, roption $ β a))
+variables (f : (Π a, part $ β a) →ₘ (Π a, part $ β a))
 
 open omega_complete_partial_order
 
-open roption (hiding ωSup) nat
+open part (hiding ωSup) nat
 open nat.upto omega_complete_partial_order
 
-lemma fix_eq_ωSup : roption.fix f = ωSup (approx_chain f) :=
+lemma fix_eq_ωSup : part.fix f = ωSup (approx_chain f) :=
 begin
   apply le_antisymm,
   { intro x, cases exists_fix_le_approx f x with i hx,
@@ -142,7 +142,7 @@ begin
     intros y x, apply approx_le_fix f },
 end
 
-lemma fix_le {X : Π a, roption $ β a} (hX : f X ≤ X) : roption.fix f ≤ X :=
+lemma fix_le {X : Π a, part $ β a} (hX : f X ≤ X) : part.fix f ≤ X :=
 begin
   rw fix_eq_ωSup f,
   apply ωSup_le _ _ _,
@@ -156,7 +156,7 @@ end
 variables {f} (hc : continuous f)
 include hc
 
-lemma fix_eq : roption.fix f = f (roption.fix f) :=
+lemma fix_eq : part.fix f = f (part.fix f) :=
 begin
   rw [fix_eq_ωSup f,hc],
   apply le_antisymm,
@@ -167,33 +167,33 @@ begin
     intros i, existsi i.succ, refl', }
 end
 
-end roption
+end part
 
-namespace roption
+namespace part
 
 /-- `to_unit` as a monotone function -/
 @[simps]
-def to_unit_mono (f : roption α →ₘ roption α) : (unit → roption α) →ₘ (unit → roption α) :=
+def to_unit_mono (f : part α →ₘ part α) : (unit → part α) →ₘ (unit → part α) :=
 { to_fun := λ x u, f (x u),
   monotone' := λ x y (h : x ≤ y) u, f.monotone $ h u }
 
-lemma to_unit_cont (f : roption α →ₘ roption α) (hc : continuous f) : continuous (to_unit_mono f)
+lemma to_unit_cont (f : part α →ₘ part α) (hc : continuous f) : continuous (to_unit_mono f)
 | c := begin
   ext ⟨⟩ : 1,
   dsimp [omega_complete_partial_order.ωSup],
   erw [hc, chain.map_comp], refl
 end
 
-noncomputable instance : lawful_fix (roption α) :=
-⟨λ f hc, show roption.fix (to_unit_mono f) () = _, by rw roption.fix_eq (to_unit_cont f hc); refl⟩
+noncomputable instance : lawful_fix (part α) :=
+⟨λ f hc, show part.fix (to_unit_mono f) () = _, by rw part.fix_eq (to_unit_cont f hc); refl⟩
 
-end roption
+end part
 
 open sigma
 
 namespace pi
 
-noncomputable instance {β} : lawful_fix (α → roption β) := ⟨λ f, roption.fix_eq⟩
+noncomputable instance {β} : lawful_fix (α → part β) := ⟨λ f, part.fix_eq⟩
 
 variables {γ : Π a : α, β a → Type*}
 
diff --git a/src/data/finmap.lean b/src/data/finmap.lean
index 2960534d245c2..7b064236817dc 100644
--- a/src/data/finmap.lean
+++ b/src/data/finmap.lean
@@ -5,7 +5,7 @@ Authors: Sean Leather, Mario Carneiro
 -/
 import data.list.alist
 import data.finset.basic
-import data.pfun
+import data.part
 /-!
 # Finite maps over `multiset`
 -/
@@ -67,8 +67,8 @@ open alist
   {γ} (s : finmap β) (f : alist β → γ)
   (H : ∀ a b : alist β, a.entries ~ b.entries → f a = f b) : γ :=
 begin
-  refine (quotient.lift_on s.1 (λ l, (⟨_, λ nd, f ⟨l, nd⟩⟩ : roption γ))
-    (λ l₁ l₂ p, roption.ext' (perm_nodupkeys p) _) : roption γ).get _,
+  refine (quotient.lift_on s.1 (λ l, (⟨_, λ nd, f ⟨l, nd⟩⟩ : part γ))
+    (λ l₁ l₂ p, part.ext' (perm_nodupkeys p) _) : part γ).get _,
   { exact λ h₁ h₂, H _ _ (by exact p) },
   { have := s.nodupkeys, rcases s.entries with ⟨l⟩, exact id }
 end
diff --git a/src/data/nat/enat.lean b/src/data/nat/enat.lean
index 958b4737bb756..3e068ca4bca83 100644
--- a/src/data/nat/enat.lean
+++ b/src/data/nat/enat.lean
@@ -30,7 +30,7 @@ with `+` and `≤`.
 
 ## Implementation details
 
-`enat` is defined to be `roption ℕ`.
+`enat` is defined to be `part ℕ`.
 
 `+` and `≤` are defined on `enat`, but there is an issue with `*` because it's not
 clear what `0 * ⊤` should be. `mul` is hence left undefined. Similarly `⊤ - ⊤` is ambiguous
@@ -45,10 +45,10 @@ followed by `@[simp] lemma to_with_top_zero'` whose proof uses `convert`.
 
 enat, with_top ℕ
 -/
-open roption
+open part
 
 /-- Type of natural numbers with infinity (`⊤`) -/
-def enat : Type := roption ℕ
+def enat : Type := part ℕ
 
 namespace enat
 
@@ -59,17 +59,17 @@ instance : has_add enat := ⟨λ x y, ⟨x.dom ∧ y.dom, λ h, get x h.1 + get
 instance : has_coe ℕ enat := ⟨some⟩
 instance (n : ℕ) : decidable (n : enat).dom := is_true trivial
 
-@[simp] lemma coe_inj {x y : ℕ} : (x : enat) = y ↔ x = y := roption.some_inj
+@[simp] lemma coe_inj {x y : ℕ} : (x : enat) = y ↔ x = y := part.some_inj
 
 @[simp] lemma dom_coe (x : ℕ) : (x : enat).dom := trivial
 
 instance : add_comm_monoid enat :=
 { add       := (+),
   zero      := (0),
-  add_comm  := λ x y, roption.ext' and.comm (λ _ _, add_comm _ _),
-  zero_add  := λ x, roption.ext' (true_and _) (λ _ _, zero_add _),
-  add_zero  := λ x, roption.ext' (and_true _) (λ _ _, add_zero _),
-  add_assoc := λ x y z, roption.ext' and.assoc (λ _ _, add_assoc _ _ _) }
+  add_comm  := λ x y, part.ext' and.comm (λ _ _, add_comm _ _),
+  zero_add  := λ x, part.ext' (true_and _) (λ _ _, zero_add _),
+  add_zero  := λ x, part.ext' (and_true _) (λ _ _, add_zero _),
+  add_assoc := λ x y z, part.ext' and.assoc (λ _ _, add_assoc _ _ _) }
 
 instance : has_le enat := ⟨λ x y, ∃ h : y.dom → x.dom, ∀ hy : y.dom, x.get (h hy) ≤ y.get hy⟩
 instance : has_top enat := ⟨none⟩
@@ -81,10 +81,10 @@ iff.rfl
 
 @[elab_as_eliminator] protected lemma cases_on {P : enat → Prop} : ∀ a : enat,
   P ⊤ → (∀ n : ℕ, P n) → P a :=
-roption.induction_on
+part.induction_on
 
 @[simp] lemma top_add (x : enat) : ⊤ + x = ⊤ :=
-roption.ext' (false_and _) (λ h, h.left.elim)
+part.ext' (false_and _) (λ h, h.left.elim)
 
 @[simp] lemma add_top (x : enat) : x + ⊤ = ⊤ :=
 by rw [add_comm, top_add]
@@ -94,7 +94,7 @@ by rw [add_comm, top_add]
 @[simp, norm_cast] lemma coe_one : ((1 : ℕ) : enat) = 1 := rfl
 
 @[simp, norm_cast] lemma coe_add (x y : ℕ) : ((x + y : ℕ) : enat) = x + y :=
-roption.ext' (and_true _).symm (λ _ _, rfl)
+part.ext' (and_true _).symm (λ _ _, rfl)
 
 lemma get_coe {x : ℕ} : get (x : enat) true.intro = x := rfl
 
@@ -107,7 +107,7 @@ lemma coe_add_get {x : ℕ} {y : enat} (h : ((x : enat) + y).dom) :
   get (x + y) h = x.get h.1 + y.get h.2 := rfl
 
 @[simp] lemma coe_get {x : enat} (h : x.dom) : (x.get h : enat) = x :=
-roption.ext' (iff_of_true trivial h) (λ _ _, rfl)
+part.ext' (iff_of_true trivial h) (λ _ _, rfl)
 
 @[simp] lemma get_zero (h : (0 : enat).dom) : (0 : enat).get h = 0 := rfl
 
@@ -135,7 +135,7 @@ instance : partial_order enat :=
   le_refl     := λ x, ⟨id, λ _, le_refl _⟩,
   le_trans    := λ x y z ⟨hxy₁, hxy₂⟩ ⟨hyz₁, hyz₂⟩,
     ⟨hxy₁ ∘ hyz₁, λ _, le_trans (hxy₂ _) (hyz₂ _)⟩,
-  le_antisymm := λ x y ⟨hxy₁, hxy₂⟩ ⟨hyx₁, hyx₂⟩, roption.ext' ⟨hyx₁, hxy₁⟩
+  le_antisymm := λ x y ⟨hxy₁, hxy₂⟩ ⟨hyx₁, hyx₂⟩, part.ext' ⟨hyx₁, hxy₁⟩
     (λ _ _, le_antisymm (hxy₂ _) (hyx₂ _)) }
 
 lemma lt_def (x y : enat) : x < y ↔ ∃ (hx : x.dom), ∀ (hy : y.dom), x.get hx < y.get hy :=
@@ -208,10 +208,10 @@ lt_of_le_of_ne le_top (λ h, absurd (congr_arg dom h) true_ne_false)
 
 @[simp] lemma coe_ne_top (x : ℕ) : (x : enat) ≠ ⊤ := ne_of_lt (coe_lt_top x)
 
-lemma ne_top_iff {x : enat} : x ≠ ⊤ ↔ ∃(n : ℕ), x = n := roption.ne_none_iff
+lemma ne_top_iff {x : enat} : x ≠ ⊤ ↔ ∃(n : ℕ), x = n := part.ne_none_iff
 
 lemma ne_top_iff_dom {x : enat} : x ≠ ⊤ ↔ x.dom :=
-by classical; exact not_iff_comm.1 roption.eq_none_iff'.symm
+by classical; exact not_iff_comm.1 part.eq_none_iff'.symm
 
 lemma ne_top_of_lt {x y : enat} (h : x < y) : x ≠ ⊤ :=
 ne_of_lt $ lt_of_lt_of_le h le_top
diff --git a/src/data/option/basic.lean b/src/data/option/basic.lean
index 227327b4c1bb7..bc5f5d48e33e5 100644
--- a/src/data/option/basic.lean
+++ b/src/data/option/basic.lean
@@ -22,7 +22,7 @@ This is useful in multiple ways:
   return `none`.
 * `option` is a monad. We love monads.
 
-`roption` is an alternative to `option` that can be seen as the type of `true`/`false` values
+`part` is an alternative to `option` that can be seen as the type of `true`/`false` values
 along with a term `a : α` if the value is `true`.
 
 ## Implementation notes
diff --git a/src/data/part.lean b/src/data/part.lean
new file mode 100644
index 0000000000000..deb48d93a9278
--- /dev/null
+++ b/src/data/part.lean
@@ -0,0 +1,387 @@
+/-
+Copyright (c) 2017 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro, Jeremy Avigad, Simon Hudon
+-/
+import data.equiv.basic
+
+/-!
+# Partial values of a type
+-/
+
+/-- `part α` is the type of "partial values" of type `α`. It
+  is similar to `option α` except the domain condition can be an
+  arbitrary proposition, not necessarily decidable. -/
+structure {u} part (α : Type u) : Type u :=
+(dom : Prop)
+(get : dom → α)
+
+namespace part
+variables {α : Type*} {β : Type*} {γ : Type*}
+
+/-- Convert a `part α` with a decidable domain to an option -/
+def to_option (o : part α) [decidable o.dom] : option α :=
+if h : dom o then some (o.get h) else none
+
+/-- `part` extensionality -/
+theorem ext' : ∀ {o p : part α}
+  (H1 : o.dom ↔ p.dom)
+  (H2 : ∀h₁ h₂, o.get h₁ = p.get h₂), o = p
+| ⟨od, o⟩ ⟨pd, p⟩ H1 H2 := have t : od = pd, from propext H1,
+  by cases t; rw [show o = p, from funext $ λp, H2 p p]
+
+/-- `part` eta expansion -/
+@[simp] theorem eta : Π (o : part α), (⟨o.dom, λ h, o.get h⟩ : part α) = o
+| ⟨h, f⟩ := rfl
+
+/-- `a ∈ o` means that `o` is defined and equal to `a` -/
+protected def mem (a : α) (o : part α) : Prop := ∃ h, o.get h = a
+
+instance : has_mem α (part α) := ⟨part.mem⟩
+
+theorem mem_eq (a : α) (o : part α) : (a ∈ o) = (∃ h, o.get h = a) :=
+rfl
+
+theorem dom_iff_mem : ∀ {o : part α}, o.dom ↔ ∃y, y ∈ o
+| ⟨p, f⟩ := ⟨λh, ⟨f h, h, rfl⟩, λ⟨_, h, rfl⟩, h⟩
+
+theorem get_mem {o : part α} (h) : get o h ∈ o := ⟨_, rfl⟩
+
+/-- `part` extensionality -/
+@[ext]
+theorem ext {o p : part α} (H : ∀ a, a ∈ o ↔ a ∈ p) : o = p :=
+ext' ⟨λ h, ((H _).1 ⟨h, rfl⟩).fst,
+     λ h, ((H _).2 ⟨h, rfl⟩).fst⟩ $
+λ a b, ((H _).2 ⟨_, rfl⟩).snd
+
+/-- The `none` value in `part` has a `false` domain and an empty function. -/
+def none : part α := ⟨false, false.rec _⟩
+
+instance : inhabited (part α) := ⟨none⟩
+
+@[simp] theorem not_mem_none (a : α) : a ∉ @none α := λ h, h.fst
+
+/-- The `some a` value in `part` has a `true` domain and the
+  function returns `a`. -/
+def some (a : α) : part α := ⟨true, λ_, a⟩
+
+theorem mem_unique : ∀ {a b : α} {o : part α}, a ∈ o → b ∈ o → a = b
+| _ _ ⟨p, f⟩ ⟨h₁, rfl⟩ ⟨h₂, rfl⟩ := rfl
+
+theorem mem.left_unique : relator.left_unique ((∈) : α → part α → Prop) :=
+⟨λ a o b, mem_unique⟩
+
+theorem get_eq_of_mem {o : part α} {a} (h : a ∈ o) (h') : get o h' = a :=
+mem_unique ⟨_, rfl⟩ h
+
+@[simp] theorem get_some {a : α} (ha : (some a).dom) : get (some a) ha = a := rfl
+
+theorem mem_some (a : α) : a ∈ some a := ⟨trivial, rfl⟩
+
+@[simp] theorem mem_some_iff {a b} : b ∈ (some a : part α) ↔ b = a :=
+⟨λ⟨h, e⟩, e.symm, λ e, ⟨trivial, e.symm⟩⟩
+
+theorem eq_some_iff {a : α} {o : part α} : o = some a ↔ a ∈ o :=
+⟨λ e, e.symm ▸ mem_some _,
+ λ ⟨h, e⟩, e ▸ ext' (iff_true_intro h) (λ _ _, rfl)⟩
+
+theorem eq_none_iff {o : part α} : o = none ↔ ∀ a, a ∉ o :=
+⟨λ e, e.symm ▸ not_mem_none,
+ λ h, ext (by simpa [not_mem_none])⟩
+
+theorem eq_none_iff' {o : part α} : o = none ↔ ¬ o.dom :=
+⟨λ e, e.symm ▸ id, λ h, eq_none_iff.2 (λ a h', h h'.fst)⟩
+
+lemma some_ne_none (x : α) : some x ≠ none :=
+by { intro h, change none.dom, rw [← h], trivial }
+
+lemma ne_none_iff {o : part α} : o ≠ none ↔ ∃x, o = some x :=
+begin
+  split,
+  { rw [ne, eq_none_iff], intro h, push_neg at h, cases h with x hx, use x, rwa [eq_some_iff] },
+  { rintro ⟨x, rfl⟩, apply some_ne_none }
+end
+
+lemma eq_none_or_eq_some (o : part α) : o = none ∨ ∃ x, o = some x :=
+begin
+  classical,
+  by_cases h : o.dom,
+  { rw dom_iff_mem at h, right,
+    apply exists_imp_exists _ h,
+    simp [eq_some_iff] },
+  { rw eq_none_iff', exact or.inl h },
+end
+
+@[simp] lemma some_inj {a b : α} : part.some a = some b ↔ a = b :=
+function.injective.eq_iff (λ a b h, congr_fun (eq_of_heq (part.mk.inj h).2) trivial)
+
+@[simp] lemma some_get {a : part α} (ha : a.dom) :
+  part.some (part.get a ha) = a :=
+eq.symm (eq_some_iff.2 ⟨ha, rfl⟩)
+
+lemma get_eq_iff_eq_some {a : part α} {ha : a.dom} {b : α} :
+  a.get ha = b ↔ a = some b :=
+⟨λ h, by simp [h.symm], λ h, by simp [h]⟩
+
+lemma get_eq_get_of_eq (a : part α) (ha : a.dom) {b : part α} (h : a = b) :
+  a.get ha = b.get (h ▸ ha) :=
+by { congr, exact h }
+
+instance none_decidable : decidable (@none α).dom := decidable.false
+instance some_decidable (a : α) : decidable (some a).dom := decidable.true
+
+/-- Retrieves the value of `a : part α` if it exists, and return the provided default value
+otherwise. -/
+def get_or_else (a : part α) [decidable a.dom] (d : α) :=
+if ha : a.dom then a.get ha else d
+
+@[simp] lemma get_or_else_none (d : α) : get_or_else none d = d :=
+dif_neg id
+
+@[simp] lemma get_or_else_some (a : α) (d : α) : get_or_else (some a) d = a :=
+dif_pos trivial
+
+@[simp] theorem mem_to_option {o : part α} [decidable o.dom] {a : α} :
+  a ∈ to_option o ↔ a ∈ o :=
+begin
+  unfold to_option,
+  by_cases h : o.dom; simp [h],
+  { exact ⟨λ h, ⟨_, h⟩, λ ⟨_, h⟩, h⟩ },
+  { exact mt Exists.fst h }
+end
+
+/-- Converts an `option α` into a `part α`. -/
+def of_option : option α → part α
+| option.none     := none
+| (option.some a) := some a
+
+@[simp] theorem mem_of_option {a : α} : ∀ {o : option α}, a ∈ of_option o ↔ a ∈ o
+| option.none     := ⟨λ h, h.fst.elim, λ h, option.no_confusion h⟩
+| (option.some b) := ⟨λ h, congr_arg option.some h.snd,
+  λ h, ⟨trivial, option.some.inj h⟩⟩
+
+@[simp] theorem of_option_dom {α} : ∀ (o : option α), (of_option o).dom ↔ o.is_some
+| option.none     := by simp [of_option, none]
+| (option.some a) := by simp [of_option]
+
+theorem of_option_eq_get {α} (o : option α) : of_option o = ⟨_, @option.get _ o⟩ :=
+part.ext' (of_option_dom o) $ λ h₁ h₂, by cases o; [cases h₁, refl]
+
+instance : has_coe (option α) (part α) := ⟨of_option⟩
+
+@[simp] theorem mem_coe {a : α} {o : option α} :
+  a ∈ (o : part α) ↔ a ∈ o := mem_of_option
+
+@[simp] theorem coe_none : (@option.none α : part α) = none := rfl
+@[simp] theorem coe_some (a : α) : (option.some a : part α) = some a := rfl
+
+@[elab_as_eliminator] protected lemma induction_on {P : part α → Prop}
+  (a : part α) (hnone : P none) (hsome : ∀ a : α, P (some a)) : P a :=
+(classical.em a.dom).elim
+  (λ h, part.some_get h ▸ hsome _)
+  (λ h, (eq_none_iff'.2 h).symm ▸ hnone)
+
+instance of_option_decidable : ∀ o : option α, decidable (of_option o).dom
+| option.none     := part.none_decidable
+| (option.some a) := part.some_decidable a
+
+@[simp] theorem to_of_option (o : option α) : to_option (of_option o) = o :=
+by cases o; refl
+
+@[simp] theorem of_to_option (o : part α) [decidable o.dom] : of_option (to_option o) = o :=
+ext $ λ a, mem_of_option.trans mem_to_option
+
+/-- `part α` is (classically) equivalent to `option α`. -/
+noncomputable def equiv_option : part α ≃ option α :=
+by haveI := classical.dec; exact
+⟨λ o, to_option o, of_option, λ o, of_to_option o,
+ λ o, eq.trans (by dsimp; congr) (to_of_option o)⟩
+
+/-- We give `part α` the order where everything is greater than `none`. -/
+instance : order_bot (part α) :=
+{ le := λ x y, ∀ i, i ∈ x → i ∈ y,
+  le_refl := λ x y, id,
+  le_trans := λ x y z f g i, g _ ∘ f _,
+  le_antisymm := λ x y f g, part.ext $ λ z, ⟨f _, g _⟩,
+  bot := none,
+  bot_le := by { introv x, rintro ⟨⟨_⟩,_⟩, } }
+
+instance : preorder (part α) :=
+by apply_instance
+
+lemma le_total_of_le_of_le {x y : part α} (z : part α) (hx : x ≤ z) (hy : y ≤ z) :
+  x ≤ y ∨ y ≤ x :=
+begin
+  rcases part.eq_none_or_eq_some x with h | ⟨b, h₀⟩,
+  { rw h, left, apply order_bot.bot_le _ },
+  right, intros b' h₁,
+  rw part.eq_some_iff at h₀,
+  replace hx := hx _ h₀, replace hy := hy _ h₁,
+  replace hx := part.mem_unique hx hy, subst hx,
+  exact h₀
+end
+
+/-- `assert p f` is a bind-like operation which appends an additional condition
+  `p` to the domain and uses `f` to produce the value. -/
+def assert (p : Prop) (f : p → part α) : part α :=
+⟨∃h : p, (f h).dom, λha, (f ha.fst).get ha.snd⟩
+
+/-- The bind operation has value `g (f.get)`, and is defined when all the
+  parts are defined. -/
+protected def bind (f : part α) (g : α → part β) : part β :=
+assert (dom f) (λb, g (f.get b))
+
+/-- The map operation for `part` just maps the value and maintains the same domain. -/
+def map (f : α → β) (o : part α) : part β :=
+⟨o.dom, f ∘ o.get⟩
+
+theorem mem_map (f : α → β) {o : part α} :
+  ∀ {a}, a ∈ o → f a ∈ map f o
+| _ ⟨h, rfl⟩ := ⟨_, rfl⟩
+
+@[simp] theorem mem_map_iff (f : α → β) {o : part α} {b} :
+  b ∈ map f o ↔ ∃ a ∈ o, f a = b :=
+⟨match b with _, ⟨h, rfl⟩ := ⟨_, ⟨_, rfl⟩, rfl⟩ end,
+ λ ⟨a, h₁, h₂⟩, h₂ ▸ mem_map f h₁⟩
+
+@[simp] theorem map_none (f : α → β) :
+  map f none = none := eq_none_iff.2 $ λ a, by simp
+
+@[simp] theorem map_some (f : α → β) (a : α) : map f (some a) = some (f a) :=
+eq_some_iff.2 $ mem_map f $ mem_some _
+
+theorem mem_assert {p : Prop} {f : p → part α}
+  : ∀ {a} (h : p), a ∈ f h → a ∈ assert p f
+| _ x ⟨h, rfl⟩ := ⟨⟨x, h⟩, rfl⟩
+
+@[simp] theorem mem_assert_iff {p : Prop} {f : p → part α} {a} :
+  a ∈ assert p f ↔ ∃ h : p, a ∈ f h :=
+⟨match a with _, ⟨h, rfl⟩ := ⟨_, ⟨_, rfl⟩⟩ end,
+ λ ⟨a, h⟩, mem_assert _ h⟩
+
+lemma assert_pos {p : Prop} {f : p → part α} (h : p) :
+  assert p f = f h :=
+begin
+  dsimp [assert],
+  cases h' : f h,
+  simp only [h', h, true_and, iff_self, exists_prop_of_true, eq_iff_iff],
+  apply function.hfunext,
+  { simp only [h,h',exists_prop_of_true] },
+  { cc }
+end
+
+lemma assert_neg {p : Prop} {f : p → part α} (h : ¬ p) :
+  assert p f = none :=
+begin
+  dsimp [assert,none], congr,
+  { simp only [h, not_false_iff, exists_prop_of_false] },
+  { apply function.hfunext,
+    { simp only [h, not_false_iff, exists_prop_of_false] },
+    cc },
+end
+
+theorem mem_bind {f : part α} {g : α → part β} :
+  ∀ {a b}, a ∈ f → b ∈ g a → b ∈ f.bind g
+| _ _ ⟨h, rfl⟩ ⟨h₂, rfl⟩ := ⟨⟨h, h₂⟩, rfl⟩
+
+@[simp] theorem mem_bind_iff {f : part α} {g : α → part β} {b} :
+  b ∈ f.bind g ↔ ∃ a ∈ f, b ∈ g a :=
+⟨match b with _, ⟨⟨h₁, h₂⟩, rfl⟩ := ⟨_, ⟨_, rfl⟩, ⟨_, rfl⟩⟩ end,
+ λ ⟨a, h₁, h₂⟩, mem_bind h₁ h₂⟩
+
+@[simp] theorem bind_none (f : α → part β) :
+  none.bind f = none := eq_none_iff.2 $ λ a, by simp
+
+@[simp] theorem bind_some (a : α) (f : α → part β) :
+  (some a).bind f = f a := ext $ by simp
+
+theorem bind_some_eq_map (f : α → β) (x : part α) :
+  x.bind (some ∘ f) = map f x :=
+ext $ by simp [eq_comm]
+
+theorem bind_assoc {γ} (f : part α) (g : α → part β) (k : β → part γ) :
+  (f.bind g).bind k = f.bind (λ x, (g x).bind k) :=
+ext $ λ a, by simp; exact
+ ⟨λ ⟨_, ⟨_, h₁, h₂⟩, h₃⟩, ⟨_, h₁, _, h₂, h₃⟩,
+  λ ⟨_, h₁, _, h₂, h₃⟩, ⟨_, ⟨_, h₁, h₂⟩, h₃⟩⟩
+
+@[simp] theorem bind_map {γ} (f : α → β) (x) (g : β → part γ) :
+  (map f x).bind g = x.bind (λ y, g (f y)) :=
+by rw [← bind_some_eq_map, bind_assoc]; simp
+
+@[simp] theorem map_bind {γ} (f : α → part β) (x : part α) (g : β → γ) :
+  map g (x.bind f) = x.bind (λ y, map g (f y)) :=
+by rw [← bind_some_eq_map, bind_assoc]; simp [bind_some_eq_map]
+
+theorem map_map (g : β → γ) (f : α → β) (o : part α) :
+  map g (map f o) = map (g ∘ f) o :=
+by rw [← bind_some_eq_map, bind_map, bind_some_eq_map]
+
+instance : monad part :=
+{ pure := @some,
+  map := @map,
+  bind := @part.bind }
+
+instance : is_lawful_monad part :=
+{ bind_pure_comp_eq_map := @bind_some_eq_map,
+  id_map := λ β f, by cases f; refl,
+  pure_bind := @bind_some,
+  bind_assoc := @bind_assoc }
+
+theorem map_id' {f : α → α} (H : ∀ (x : α), f x = x) (o) : map f o = o :=
+by rw [show f = id, from funext H]; exact id_map o
+
+@[simp] theorem bind_some_right (x : part α) : x.bind some = x :=
+by rw [bind_some_eq_map]; simp [map_id']
+
+@[simp] theorem pure_eq_some (a : α) : pure a = some a := rfl
+@[simp] theorem ret_eq_some (a : α) : return a = some a := rfl
+
+@[simp] theorem map_eq_map {α β} (f : α → β) (o : part α) :
+  f <$> o = map f o := rfl
+
+@[simp] theorem bind_eq_bind {α β} (f : part α) (g : α → part β) :
+  f >>= g = f.bind g := rfl
+
+lemma bind_le {α} (x : part α) (f : α → part β) (y : part β) :
+  x >>= f ≤ y ↔ (∀ a, a ∈ x → f a ≤ y) :=
+begin
+  split; intro h,
+  { intros a h' b, replace h := h b,
+    simp only [and_imp, exists_prop, bind_eq_bind, mem_bind_iff, exists_imp_distrib] at h,
+    apply h _ h' },
+  { intros b h',
+    simp only [exists_prop, bind_eq_bind, mem_bind_iff] at h',
+    rcases h' with ⟨a,h₀,h₁⟩, apply h _ h₀ _ h₁ },
+end
+
+instance : monad_fail part :=
+{ fail := λ_ _, none, ..part.monad }
+
+/-- `restrict p o h` replaces the domain of `o` with `p`, and is well defined when
+  `p` implies `o` is defined. -/
+def restrict (p : Prop) : ∀ (o : part α), (p → o.dom) → part α
+| ⟨d, f⟩ H := ⟨p, λh, f (H h)⟩
+
+@[simp]
+theorem mem_restrict (p : Prop) (o : part α) (h : p → o.dom) (a : α) :
+  a ∈ restrict p o h ↔ p ∧ a ∈ o :=
+begin
+  cases o, dsimp [restrict, mem_eq], split,
+  { rintro ⟨h₀, h₁⟩, exact ⟨h₀, ⟨_, h₁⟩⟩ },
+  rintro ⟨h₀, h₁, h₂⟩, exact ⟨h₀, h₂⟩
+end
+
+/-- `unwrap o` gets the value at `o`, ignoring the condition. This function is unsound. -/
+meta def unwrap (o : part α) : α := o.get undefined
+
+theorem assert_defined {p : Prop} {f : p → part α} :
+  ∀ (h : p), (f h).dom → (assert p f).dom := exists.intro
+
+theorem bind_defined {f : part α} {g : α → part β} :
+  ∀ (h : f.dom), (g (f.get h)).dom → (f.bind g).dom := assert_defined
+
+@[simp] theorem bind_dom {f : part α} {g : α → part β} :
+  (f.bind g).dom ↔ ∃ h : f.dom, (g (f.get h)).dom := iff.rfl
+
+end part
diff --git a/src/data/pfun.lean b/src/data/pfun.lean
index 94cb1ea8ca998..683293b81a7d2 100644
--- a/src/data/pfun.lean
+++ b/src/data/pfun.lean
@@ -3,398 +3,29 @@ Copyright (c) 2017 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Jeremy Avigad, Simon Hudon
 -/
+import data.part
 import data.rel
 
-/-- `roption α` is the type of "partial values" of type `α`. It
-  is similar to `option α` except the domain condition can be an
-  arbitrary proposition, not necessarily decidable. -/
-structure {u} roption (α : Type u) : Type u :=
-(dom : Prop)
-(get : dom → α)
-
-namespace roption
-variables {α : Type*} {β : Type*} {γ : Type*}
-
-/-- Convert an `roption α` with a decidable domain to an option -/
-def to_option (o : roption α) [decidable o.dom] : option α :=
-if h : dom o then some (o.get h) else none
-
-/-- `roption` extensionality -/
-theorem ext' : ∀ {o p : roption α}
-  (H1 : o.dom ↔ p.dom)
-  (H2 : ∀h₁ h₂, o.get h₁ = p.get h₂), o = p
-| ⟨od, o⟩ ⟨pd, p⟩ H1 H2 := have t : od = pd, from propext H1,
-  by cases t; rw [show o = p, from funext $ λp, H2 p p]
-
-/-- `roption` eta expansion -/
-@[simp] theorem eta : Π (o : roption α), (⟨o.dom, λ h, o.get h⟩ : roption α) = o
-| ⟨h, f⟩ := rfl
-
-/-- `a ∈ o` means that `o` is defined and equal to `a` -/
-protected def mem (a : α) (o : roption α) : Prop := ∃ h, o.get h = a
-
-instance : has_mem α (roption α) := ⟨roption.mem⟩
-
-theorem mem_eq (a : α) (o : roption α) : (a ∈ o) = (∃ h, o.get h = a) :=
-rfl
-
-theorem dom_iff_mem : ∀ {o : roption α}, o.dom ↔ ∃y, y ∈ o
-| ⟨p, f⟩ := ⟨λh, ⟨f h, h, rfl⟩, λ⟨_, h, rfl⟩, h⟩
-
-theorem get_mem {o : roption α} (h) : get o h ∈ o := ⟨_, rfl⟩
-
-/-- `roption` extensionality -/
-@[ext]
-theorem ext {o p : roption α} (H : ∀ a, a ∈ o ↔ a ∈ p) : o = p :=
-ext' ⟨λ h, ((H _).1 ⟨h, rfl⟩).fst,
-     λ h, ((H _).2 ⟨h, rfl⟩).fst⟩ $
-λ a b, ((H _).2 ⟨_, rfl⟩).snd
-
-/-- The `none` value in `roption` has a `false` domain and an empty function. -/
-def none : roption α := ⟨false, false.rec _⟩
-
-instance : inhabited (roption α) := ⟨none⟩
-
-@[simp] theorem not_mem_none (a : α) : a ∉ @none α := λ h, h.fst
-
-/-- The `some a` value in `roption` has a `true` domain and the
-  function returns `a`. -/
-def some (a : α) : roption α := ⟨true, λ_, a⟩
-
-theorem mem_unique : ∀ {a b : α} {o : roption α}, a ∈ o → b ∈ o → a = b
-| _ _ ⟨p, f⟩ ⟨h₁, rfl⟩ ⟨h₂, rfl⟩ := rfl
-
-theorem mem.left_unique : relator.left_unique ((∈) : α → roption α → Prop) :=
-⟨λ a o b, mem_unique⟩
-
-theorem get_eq_of_mem {o : roption α} {a} (h : a ∈ o) (h') : get o h' = a :=
-mem_unique ⟨_, rfl⟩ h
-
-@[simp] theorem get_some {a : α} (ha : (some a).dom) : get (some a) ha = a := rfl
-
-theorem mem_some (a : α) : a ∈ some a := ⟨trivial, rfl⟩
-
-@[simp] theorem mem_some_iff {a b} : b ∈ (some a : roption α) ↔ b = a :=
-⟨λ⟨h, e⟩, e.symm, λ e, ⟨trivial, e.symm⟩⟩
-
-theorem eq_some_iff {a : α} {o : roption α} : o = some a ↔ a ∈ o :=
-⟨λ e, e.symm ▸ mem_some _,
- λ ⟨h, e⟩, e ▸ ext' (iff_true_intro h) (λ _ _, rfl)⟩
-
-theorem eq_none_iff {o : roption α} : o = none ↔ ∀ a, a ∉ o :=
-⟨λ e, e.symm ▸ not_mem_none,
- λ h, ext (by simpa [not_mem_none])⟩
-
-theorem eq_none_iff' {o : roption α} : o = none ↔ ¬ o.dom :=
-⟨λ e, e.symm ▸ id, λ h, eq_none_iff.2 (λ a h', h h'.fst)⟩
-
-lemma some_ne_none (x : α) : some x ≠ none :=
-by { intro h, change none.dom, rw [← h], trivial }
-
-lemma ne_none_iff {o : roption α} : o ≠ none ↔ ∃x, o = some x :=
-begin
-  split,
-  { rw [ne, eq_none_iff], intro h, push_neg at h, cases h with x hx, use x, rwa [eq_some_iff] },
-  { rintro ⟨x, rfl⟩, apply some_ne_none }
-end
-
-lemma eq_none_or_eq_some (o : roption α) : o = none ∨ ∃ x, o = some x :=
-begin
-  classical,
-  by_cases h : o.dom,
-  { rw dom_iff_mem at h, right,
-    apply exists_imp_exists _ h,
-    simp [eq_some_iff] },
-  { rw eq_none_iff', exact or.inl h },
-end
-
-@[simp] lemma some_inj {a b : α} : roption.some a = some b ↔ a = b :=
-function.injective.eq_iff (λ a b h, congr_fun (eq_of_heq (roption.mk.inj h).2) trivial)
-
-@[simp] lemma some_get {a : roption α} (ha : a.dom) :
-  roption.some (roption.get a ha) = a :=
-eq.symm (eq_some_iff.2 ⟨ha, rfl⟩)
-
-lemma get_eq_iff_eq_some {a : roption α} {ha : a.dom} {b : α} :
-  a.get ha = b ↔ a = some b :=
-⟨λ h, by simp [h.symm], λ h, by simp [h]⟩
-
-lemma get_eq_get_of_eq (a : roption α) (ha : a.dom) {b : roption α} (h : a = b) :
-  a.get ha = b.get (h ▸ ha) :=
-by { congr, exact h }
-
-instance none_decidable : decidable (@none α).dom := decidable.false
-instance some_decidable (a : α) : decidable (some a).dom := decidable.true
-
-def get_or_else (a : roption α) [decidable a.dom] (d : α) :=
-if ha : a.dom then a.get ha else d
-
-@[simp] lemma get_or_else_none (d : α) : get_or_else none d = d :=
-dif_neg id
-
-@[simp] lemma get_or_else_some (a : α) (d : α) : get_or_else (some a) d = a :=
-dif_pos trivial
-
-@[simp] theorem mem_to_option {o : roption α} [decidable o.dom] {a : α} :
-  a ∈ to_option o ↔ a ∈ o :=
-begin
-  unfold to_option,
-  by_cases h : o.dom; simp [h],
-  { exact ⟨λ h, ⟨_, h⟩, λ ⟨_, h⟩, h⟩ },
-  { exact mt Exists.fst h }
-end
-
-/-- Convert an `option α` into an `roption α` -/
-def of_option : option α → roption α
-| option.none     := none
-| (option.some a) := some a
-
-@[simp] theorem mem_of_option {a : α} : ∀ {o : option α}, a ∈ of_option o ↔ a ∈ o
-| option.none     := ⟨λ h, h.fst.elim, λ h, option.no_confusion h⟩
-| (option.some b) := ⟨λ h, congr_arg option.some h.snd,
-  λ h, ⟨trivial, option.some.inj h⟩⟩
-
-@[simp] theorem of_option_dom {α} : ∀ (o : option α), (of_option o).dom ↔ o.is_some
-| option.none     := by simp [of_option, none]
-| (option.some a) := by simp [of_option]
-
-theorem of_option_eq_get {α} (o : option α) : of_option o = ⟨_, @option.get _ o⟩ :=
-roption.ext' (of_option_dom o) $ λ h₁ h₂, by cases o; [cases h₁, refl]
-
-instance : has_coe (option α) (roption α) := ⟨of_option⟩
-
-@[simp] theorem mem_coe {a : α} {o : option α} :
-  a ∈ (o : roption α) ↔ a ∈ o := mem_of_option
-
-@[simp] theorem coe_none : (@option.none α : roption α) = none := rfl
-@[simp] theorem coe_some (a : α) : (option.some a : roption α) = some a := rfl
-
-@[elab_as_eliminator] protected lemma induction_on {P : roption α → Prop}
-  (a : roption α) (hnone : P none) (hsome : ∀ a : α, P (some a)) : P a :=
-(classical.em a.dom).elim
-  (λ h, roption.some_get h ▸ hsome _)
-  (λ h, (eq_none_iff'.2 h).symm ▸ hnone)
-
-instance of_option_decidable : ∀ o : option α, decidable (of_option o).dom
-| option.none     := roption.none_decidable
-| (option.some a) := roption.some_decidable a
-
-@[simp] theorem to_of_option (o : option α) : to_option (of_option o) = o :=
-by cases o; refl
-
-@[simp] theorem of_to_option (o : roption α) [decidable o.dom] : of_option (to_option o) = o :=
-ext $ λ a, mem_of_option.trans mem_to_option
-
-noncomputable def equiv_option : roption α ≃ option α :=
-by haveI := classical.dec; exact
-⟨λ o, to_option o, of_option, λ o, of_to_option o,
- λ o, eq.trans (by dsimp; congr) (to_of_option o)⟩
-
-instance : order_bot (roption α) :=
-{ le := λ x y, ∀ i, i ∈ x → i ∈ y,
-  le_refl := λ x y, id,
-  le_trans := λ x y z f g i, g _ ∘ f _,
-  le_antisymm := λ x y f g, roption.ext $ λ z, ⟨f _, g _⟩,
-  bot := none,
-  bot_le := by { introv x, rintro ⟨⟨_⟩,_⟩, } }
-
-instance : preorder (roption α) :=
-by apply_instance
-
-lemma le_total_of_le_of_le {x y : roption α} (z : roption α) (hx : x ≤ z) (hy : y ≤ z) :
-  x ≤ y ∨ y ≤ x :=
-begin
-  rcases roption.eq_none_or_eq_some x with h | ⟨b, h₀⟩,
-  { rw h, left, apply order_bot.bot_le _ },
-  right, intros b' h₁,
-  rw roption.eq_some_iff at h₀,
-  replace hx := hx _ h₀, replace hy := hy _ h₁,
-  replace hx := roption.mem_unique hx hy, subst hx,
-  exact h₀
-end
-
-/-- `assert p f` is a bind-like operation which appends an additional condition
-  `p` to the domain and uses `f` to produce the value. -/
-def assert (p : Prop) (f : p → roption α) : roption α :=
-⟨∃h : p, (f h).dom, λha, (f ha.fst).get ha.snd⟩
-
-/-- The bind operation has value `g (f.get)`, and is defined when all the
-  parts are defined. -/
-protected def bind (f : roption α) (g : α → roption β) : roption β :=
-assert (dom f) (λb, g (f.get b))
-
-/-- The map operation for `roption` just maps the value and maintains the same domain. -/
-def map (f : α → β) (o : roption α) : roption β :=
-⟨o.dom, f ∘ o.get⟩
-
-theorem mem_map (f : α → β) {o : roption α} :
-  ∀ {a}, a ∈ o → f a ∈ map f o
-| _ ⟨h, rfl⟩ := ⟨_, rfl⟩
-
-@[simp] theorem mem_map_iff (f : α → β) {o : roption α} {b} :
-  b ∈ map f o ↔ ∃ a ∈ o, f a = b :=
-⟨match b with _, ⟨h, rfl⟩ := ⟨_, ⟨_, rfl⟩, rfl⟩ end,
- λ ⟨a, h₁, h₂⟩, h₂ ▸ mem_map f h₁⟩
-
-@[simp] theorem map_none (f : α → β) :
-  map f none = none := eq_none_iff.2 $ λ a, by simp
-
-@[simp] theorem map_some (f : α → β) (a : α) : map f (some a) = some (f a) :=
-eq_some_iff.2 $ mem_map f $ mem_some _
-
-theorem mem_assert {p : Prop} {f : p → roption α}
-  : ∀ {a} (h : p), a ∈ f h → a ∈ assert p f
-| _ x ⟨h, rfl⟩ := ⟨⟨x, h⟩, rfl⟩
-
-@[simp] theorem mem_assert_iff {p : Prop} {f : p → roption α} {a} :
-  a ∈ assert p f ↔ ∃ h : p, a ∈ f h :=
-⟨match a with _, ⟨h, rfl⟩ := ⟨_, ⟨_, rfl⟩⟩ end,
- λ ⟨a, h⟩, mem_assert _ h⟩
-
-lemma assert_pos {p : Prop} {f : p → roption α} (h : p) :
-  assert p f = f h :=
-begin
-  dsimp [assert],
-  cases h' : f h,
-  simp only [h', h, true_and, iff_self, exists_prop_of_true, eq_iff_iff],
-  apply function.hfunext,
-  { simp only [h,h',exists_prop_of_true] },
-  { cc }
-end
-
-lemma assert_neg {p : Prop} {f : p → roption α} (h : ¬ p) :
-  assert p f = none :=
-begin
-  dsimp [assert,none], congr,
-  { simp only [h, not_false_iff, exists_prop_of_false] },
-  { apply function.hfunext,
-    { simp only [h, not_false_iff, exists_prop_of_false] },
-    cc },
-end
-
-theorem mem_bind {f : roption α} {g : α → roption β} :
-  ∀ {a b}, a ∈ f → b ∈ g a → b ∈ f.bind g
-| _ _ ⟨h, rfl⟩ ⟨h₂, rfl⟩ := ⟨⟨h, h₂⟩, rfl⟩
-
-@[simp] theorem mem_bind_iff {f : roption α} {g : α → roption β} {b} :
-  b ∈ f.bind g ↔ ∃ a ∈ f, b ∈ g a :=
-⟨match b with _, ⟨⟨h₁, h₂⟩, rfl⟩ := ⟨_, ⟨_, rfl⟩, ⟨_, rfl⟩⟩ end,
- λ ⟨a, h₁, h₂⟩, mem_bind h₁ h₂⟩
-
-@[simp] theorem bind_none (f : α → roption β) :
-  none.bind f = none := eq_none_iff.2 $ λ a, by simp
-
-@[simp] theorem bind_some (a : α) (f : α → roption β) :
-  (some a).bind f = f a := ext $ by simp
-
-theorem bind_some_eq_map (f : α → β) (x : roption α) :
-  x.bind (some ∘ f) = map f x :=
-ext $ by simp [eq_comm]
-
-theorem bind_assoc {γ} (f : roption α) (g : α → roption β) (k : β → roption γ) :
-  (f.bind g).bind k = f.bind (λ x, (g x).bind k) :=
-ext $ λ a, by simp; exact
- ⟨λ ⟨_, ⟨_, h₁, h₂⟩, h₃⟩, ⟨_, h₁, _, h₂, h₃⟩,
-  λ ⟨_, h₁, _, h₂, h₃⟩, ⟨_, ⟨_, h₁, h₂⟩, h₃⟩⟩
-
-@[simp] theorem bind_map {γ} (f : α → β) (x) (g : β → roption γ) :
-  (map f x).bind g = x.bind (λ y, g (f y)) :=
-by rw [← bind_some_eq_map, bind_assoc]; simp
-
-@[simp] theorem map_bind {γ} (f : α → roption β) (x : roption α) (g : β → γ) :
-  map g (x.bind f) = x.bind (λ y, map g (f y)) :=
-by rw [← bind_some_eq_map, bind_assoc]; simp [bind_some_eq_map]
-
-theorem map_map (g : β → γ) (f : α → β) (o : roption α) :
-  map g (map f o) = map (g ∘ f) o :=
-by rw [← bind_some_eq_map, bind_map, bind_some_eq_map]
-
-instance : monad roption :=
-{ pure := @some,
-  map := @map,
-  bind := @roption.bind }
-
-instance : is_lawful_monad roption :=
-{ bind_pure_comp_eq_map := @bind_some_eq_map,
-  id_map := λ β f, by cases f; refl,
-  pure_bind := @bind_some,
-  bind_assoc := @bind_assoc }
-
-theorem map_id' {f : α → α} (H : ∀ (x : α), f x = x) (o) : map f o = o :=
-by rw [show f = id, from funext H]; exact id_map o
-
-@[simp] theorem bind_some_right (x : roption α) : x.bind some = x :=
-by rw [bind_some_eq_map]; simp [map_id']
-
-@[simp] theorem pure_eq_some (a : α) : pure a = some a := rfl
-@[simp] theorem ret_eq_some (a : α) : return a = some a := rfl
-
-@[simp] theorem map_eq_map {α β} (f : α → β) (o : roption α) :
-  f <$> o = map f o := rfl
-
-@[simp] theorem bind_eq_bind {α β} (f : roption α) (g : α → roption β) :
-  f >>= g = f.bind g := rfl
-
-lemma bind_le {α} (x : roption α) (f : α → roption β) (y : roption β) :
-  x >>= f ≤ y ↔ (∀ a, a ∈ x → f a ≤ y) :=
-begin
-  split; intro h,
-  { intros a h' b, replace h := h b,
-    simp only [and_imp, exists_prop, bind_eq_bind, mem_bind_iff, exists_imp_distrib] at h,
-    apply h _ h' },
-  { intros b h',
-    simp only [exists_prop, bind_eq_bind, mem_bind_iff] at h',
-    rcases h' with ⟨a,h₀,h₁⟩, apply h _ h₀ _ h₁ },
-end
-
-instance : monad_fail roption :=
-{ fail := λ_ _, none, ..roption.monad }
-
-/- `restrict p o h` replaces the domain of `o` with `p`, and is well defined when
-  `p` implies `o` is defined. -/
-def restrict (p : Prop) : ∀ (o : roption α), (p → o.dom) → roption α
-| ⟨d, f⟩ H := ⟨p, λh, f (H h)⟩
-
-@[simp]
-theorem mem_restrict (p : Prop) (o : roption α) (h : p → o.dom) (a : α) :
-  a ∈ restrict p o h ↔ p ∧ a ∈ o :=
-begin
-  cases o, dsimp [restrict, mem_eq], split,
-  { rintro ⟨h₀, h₁⟩, exact ⟨h₀, ⟨_, h₁⟩⟩ },
-  rintro ⟨h₀, h₁, h₂⟩, exact ⟨h₀, h₂⟩
-end
-
-/-- `unwrap o` gets the value at `o`, ignoring the condition.
-  (This function is unsound.) -/
-meta def unwrap (o : roption α) : α := o.get undefined
-
-theorem assert_defined {p : Prop} {f : p → roption α} :
-  ∀ (h : p), (f h).dom → (assert p f).dom := exists.intro
-
-theorem bind_defined {f : roption α} {g : α → roption β} :
-  ∀ (h : f.dom), (g (f.get h)).dom → (f.bind g).dom := assert_defined
-
-@[simp] theorem bind_dom {f : roption α} {g : α → roption β} :
-  (f.bind g).dom ↔ ∃ h : f.dom, (g (f.get h)).dom := iff.rfl
-
-end roption
+/-!
+# Partial functions
+-/
 
 /-- `pfun α β`, or `α →. β`, is the type of partial functions from
-  `α` to `β`. It is defined as `α → roption β`. -/
-def pfun (α : Type*) (β : Type*) := α → roption β
+  `α` to `β`. It is defined as `α → part β`. -/
+def pfun (α : Type*) (β : Type*) := α → part β
 
 infixr ` →. `:25 := pfun
 
 namespace pfun
 variables {α : Type*} {β : Type*} {γ : Type*}
 
-instance : inhabited (α →. β) := ⟨λ a, roption.none⟩
+instance : inhabited (α →. β) := ⟨λ a, part.none⟩
 
 /-- The domain of a partial function -/
 def dom (f : α →. β) : set α := {a | (f a).dom}
 
 theorem mem_dom (f : α →. β) (x : α) : x ∈ dom f ↔ ∃ y, y ∈ f x :=
-by simp [dom, roption.dom_iff_mem]
+by simp [dom, part.dom_iff_mem]
 
 theorem dom_eq (f : α →. β) : dom f = {x | ∃ y, y ∈ f x} :=
 set.ext (mem_dom f)
@@ -404,16 +35,16 @@ def fn (f : α →. β) (x) (h : dom f x) : β := (f x).get h
 
 /-- Evaluate a partial function to return an `option` -/
 def eval_opt (f : α →. β) [D : decidable_pred (∈ dom f)] (x : α) : option β :=
-@roption.to_option _ _ (D x)
+@part.to_option _ _ (D x)
 
 /-- Partial function extensionality -/
 theorem ext' {f g : α →. β}
   (H1 : ∀ a, a ∈ dom f ↔ a ∈ dom g)
   (H2 : ∀ a p q, f.fn a p = g.fn a q) : f = g :=
-funext $ λ a, roption.ext' (H1 a) (H2 a)
+funext $ λ a, part.ext' (H1 a) (H2 a)
 
 theorem ext {f g : α →. β} (H : ∀ a b, b ∈ f a ↔ b ∈ g a) : f = g :=
-funext $ λ a, roption.ext (H a)
+funext $ λ a, part.ext (H a)
 
 /-- Turn a partial function into a function out of a subtype -/
 def as_subtype (f : α →. β) (s : f.dom) : β := f.fn s s.2
@@ -423,22 +54,22 @@ the set of pairs `(p : α → Prop, f : subtype p → β)`. -/
 def equiv_subtype : (α →. β) ≃ (Σ p : α → Prop, subtype p → β) :=
 ⟨λ f, ⟨λ a, (f a).dom, as_subtype f⟩,
  λ f x, ⟨f.1 x, λ h, f.2 ⟨x, h⟩⟩,
- λ f, funext $ λ a, roption.eta _,
+ λ f, funext $ λ a, part.eta _,
  λ ⟨p, f⟩, by dsimp; congr; funext a; cases a; refl⟩
 
 theorem as_subtype_eq_of_mem {f : α →. β} {x : α} {y : β} (fxy : y ∈ f x) (domx : x ∈ f.dom) :
   f.as_subtype ⟨x, domx⟩ = y :=
-roption.mem_unique (roption.get_mem _) fxy
+part.mem_unique (part.get_mem _) fxy
 
 /-- Turn a total function into a partial function -/
-protected def lift (f : α → β) : α →. β := λ a, roption.some (f a)
+protected def lift (f : α → β) : α →. β := λ a, part.some (f a)
 
 instance : has_coe (α → β) (α →. β) := ⟨pfun.lift⟩
 
 @[simp] theorem lift_eq_coe (f : α → β) : pfun.lift f = f := rfl
 
 @[simp] theorem coe_val (f : α → β) (a : α) :
-  (f : α →. β) a = roption.some (f a) := rfl
+  (f : α →. β) a = part.some (f a) := rfl
 
 /-- The graph of a partial function is the set of pairs
   `(x, f x)` where `x` is in the domain of `f`. -/
@@ -452,7 +83,7 @@ def ran (f : α →. β) : set β := {b | ∃a, b ∈ f a}
 
 /-- Restrict a partial function to a smaller domain. -/
 def restrict (f : α →. β) {p : set α} (H : p ⊆ f.dom) : α →. β :=
-λ x, roption.restrict (x ∈ p) (f x) (@H x)
+λ x, part.restrict (x ∈ p) (f x) (@H x)
 
 @[simp]
 theorem mem_restrict {f : α →. β} {s : set α} (h : s ⊆ f.dom) (a : α) (b : β) :
@@ -470,21 +101,21 @@ theorem res_univ (f : α → β) : pfun.res f set.univ = f :=
 rfl
 
 theorem dom_iff_graph (f : α →. β) (x : α) : x ∈ f.dom ↔ ∃y, (x, y) ∈ f.graph :=
-roption.dom_iff_mem
+part.dom_iff_mem
 
 theorem lift_graph {f : α → β} {a b} : (a, b) ∈ (f : α →. β).graph ↔ f a = b :=
 show (∃ (h : true), f a = b) ↔ f a = b, by simp
 
 /-- The monad `pure` function, the total constant `x` function -/
-protected def pure (x : β) : α →. β := λ_, roption.some x
+protected def pure (x : β) : α →. β := λ_, part.some x
 
-/-- The monad `bind` function, pointwise `roption.bind` -/
+/-- The monad `bind` function, pointwise `part.bind` -/
 def bind (f : α →. β) (g : β → α →. γ) : α →. γ :=
-λa, roption.bind (f a) (λb, g b a)
+λa, part.bind (f a) (λb, g b a)
 
-/-- The monad `map` function, pointwise `roption.map` -/
+/-- The monad `map` function, pointwise `part.map` -/
 def map (f : β → γ) (g : α →. β) : α →. γ :=
-λa, roption.map f (g a)
+λa, part.map f (g a)
 
 instance : monad (pfun α) :=
 { pure := @pfun.pure _,
@@ -492,11 +123,11 @@ instance : monad (pfun α) :=
   map := @pfun.map _ }
 
 instance : is_lawful_monad (pfun α) :=
-{ bind_pure_comp_eq_map := λ β γ f x, funext $ λ a, roption.bind_some_eq_map _ _,
+{ bind_pure_comp_eq_map := λ β γ f x, funext $ λ a, part.bind_some_eq_map _ _,
   id_map := λ β f, by funext a; dsimp [functor.map, pfun.map]; cases f a; refl,
-  pure_bind := λ β γ x f, funext $ λ a, roption.bind_some.{u_1 u_2} _ (f x),
+  pure_bind := λ β γ x f, funext $ λ a, part.bind_some.{u_1 u_2} _ (f x),
   bind_assoc := λ β γ δ f g k,
-    funext $ λ a, roption.bind_assoc (f a) (λ b, g b a) (λ b, k b a) }
+    funext $ λ a, part.bind_assoc (f a) (λ b, g b a) (λ b, k b a) }
 
 theorem pure_defined (p : set α) (x : β) : p ⊆ (@pfun.pure α _ x).dom := set.subset_univ p
 
@@ -505,38 +136,38 @@ theorem bind_defined {α β γ} (p : set α) {f : α →. β} {g : β → α →
 λa ha, (⟨H1 ha, H2 _ ha⟩ : (f >>= g).dom a)
 
 def fix (f : α →. β ⊕ α) : α →. β := λ a,
-roption.assert (acc (λ x y, sum.inr x ∈ f y) a) $ λ h,
+part.assert (acc (λ x y, sum.inr x ∈ f y) a) $ λ h,
 @well_founded.fix_F _ (λ x y, sum.inr x ∈ f y) _
-  (λ a IH, roption.assert (f a).dom $ λ hf,
+  (λ a IH, part.assert (f a).dom $ λ hf,
     by cases e : (f a).get hf with b a';
-      [exact roption.some b, exact IH _ ⟨hf, e⟩])
+      [exact part.some b, exact IH _ ⟨hf, e⟩])
   a h
 
 theorem dom_of_mem_fix {f : α →. β ⊕ α} {a : α} {b : β}
   (h : b ∈ fix f a) : (f a).dom :=
-let ⟨h₁, h₂⟩ := roption.mem_assert_iff.1 h in
+let ⟨h₁, h₂⟩ := part.mem_assert_iff.1 h in
 by rw well_founded.fix_F_eq at h₂; exact h₂.fst.fst
 
 theorem mem_fix_iff {f : α →. β ⊕ α} {a : α} {b : β} :
   b ∈ fix f a ↔ sum.inl b ∈ f a ∨ ∃ a', sum.inr a' ∈ f a ∧ b ∈ fix f a' :=
-⟨λ h, let ⟨h₁, h₂⟩ := roption.mem_assert_iff.1 h in
+⟨λ h, let ⟨h₁, h₂⟩ := part.mem_assert_iff.1 h in
   begin
     rw well_founded.fix_F_eq at h₂,
     simp at h₂,
     cases h₂ with h₂ h₃,
     cases e : (f a).get h₂ with b' a'; simp [e] at h₃,
     { subst b', refine or.inl ⟨h₂, e⟩ },
-    { exact or.inr ⟨a', ⟨_, e⟩, roption.mem_assert _ h₃⟩ }
+    { exact or.inr ⟨a', ⟨_, e⟩, part.mem_assert _ h₃⟩ }
   end,
 λ h, begin
   simp [fix],
   rcases h with ⟨h₁, h₂⟩ | ⟨a', h, h₃⟩,
   { refine ⟨⟨_, λ y h', _⟩, _⟩,
-    { injection roption.mem_unique ⟨h₁, h₂⟩ h' },
+    { injection part.mem_unique ⟨h₁, h₂⟩ h' },
     { rw well_founded.fix_F_eq, simp [h₁, h₂] } },
   { simp [fix] at h₃, cases h₃ with h₃ h₄,
     refine ⟨⟨_, λ y h', _⟩, _⟩,
-    { injection roption.mem_unique h h' with e,
+    { injection part.mem_unique h h' with e,
       exact e ▸ h₃ },
     { cases h with h₁ h₂,
       rw well_founded.fix_F_eq, simp [h₁, h₂, h₄] } }
@@ -547,12 +178,12 @@ end⟩
   (H : ∀ a, b ∈ fix f a →
     (∀ a', b ∈ fix f a' → sum.inr a' ∈ f a → C a') → C a) : C a :=
 begin
-  replace h := roption.mem_assert_iff.1 h,
+  replace h := part.mem_assert_iff.1 h,
   have := h.snd, revert this,
   induction h.fst with a ha IH, intro h₂,
-  refine H a (roption.mem_assert_iff.2 ⟨⟨_, ha⟩, h₂⟩)
+  refine H a (part.mem_assert_iff.2 ⟨⟨_, ha⟩, h₂⟩)
     (λ a' ha' fa', _),
-  have := (roption.mem_assert_iff.1 ha').snd,
+  have := (part.mem_assert_iff.1 ha').snd,
   exact IH _ fa' ⟨ha _ fa', this⟩ this
 end
 
@@ -586,7 +217,7 @@ lemma mem_preimage (s : set β) (x : α) : x ∈ preimage f s ↔ ∃ y ∈ s, y
 iff.rfl
 
 lemma preimage_subset_dom (s : set β) : f.preimage s ⊆ f.dom :=
-assume x ⟨y, ys, fxy⟩, roption.dom_iff_mem.mpr ⟨y, fxy⟩
+assume x ⟨y, ys, fxy⟩, part.dom_iff_mem.mpr ⟨y, fxy⟩
 
 lemma preimage_mono {s t : set β} (h : s ⊆ t) : f.preimage s ⊆ f.preimage t :=
 rel.preimage_mono _ h
@@ -634,7 +265,7 @@ by ext x; simp [core_def]
 
 lemma preimage_subset_core (f : α →. β) (s : set β) : f.preimage s ⊆ f.core s :=
 assume x ⟨y, ys, fxy⟩ y' fxy',
-have y = y', from roption.mem_unique fxy fxy',
+have y = y', from part.mem_unique fxy fxy',
 this ▸ ys
 
 lemma preimage_eq (f : α →. β) (s : set β) : f.preimage s = f.core s ∩ f.dom :=
@@ -642,8 +273,8 @@ set.eq_of_subset_of_subset
   (set.subset_inter (preimage_subset_core f s) (preimage_subset_dom f s))
   (assume x ⟨xcore, xdom⟩,
     let y := (f x).get xdom in
-    have ys : y ∈ s, from xcore _ (roption.get_mem _),
-    show x ∈ preimage f s, from  ⟨(f x).get xdom, ys, roption.get_mem _⟩)
+    have ys : y ∈ s, from xcore _ (part.get_mem _),
+    show x ∈ preimage f s, from  ⟨(f x).get xdom, ys, part.get_mem _⟩)
 
 lemma core_eq (f : α →. β) (s : set β) : f.core s = f.preimage s ∪ f.domᶜ :=
 by rw [preimage_eq, set.union_distrib_right, set.union_comm (dom f), set.compl_union_self,
@@ -656,10 +287,10 @@ begin
   simp only [set.mem_preimage, set.mem_set_of_eq, pfun.as_subtype, pfun.mem_preimage],
   show pfun.fn f (x.val) _ ∈ s ↔ ∃ y ∈ s, y ∈ f (x.val),
   exact iff.intro
-    (assume h, ⟨_, h, roption.get_mem _⟩)
+    (assume h, ⟨_, h, part.get_mem _⟩)
     (assume ⟨y, ys, fxy⟩,
-      have f.fn x.val x.property ∈ f x.val := roption.get_mem _,
-      roption.mem_unique fxy this ▸ ys)
+      have f.fn x.val x.property ∈ f x.val := part.get_mem _,
+      part.mem_unique fxy this ▸ ys)
 end
 
 end pfun
diff --git a/src/data/polynomial/div.lean b/src/data/polynomial/div.lean
index 15dc25ba94174..7837133e94efd 100644
--- a/src/data/polynomial/div.lean
+++ b/src/data/polynomial/div.lean
@@ -438,7 +438,7 @@ by exactI nat.find (multiplicity_X_sub_C_finite a h0)
 lemma root_multiplicity_eq_multiplicity (p : polynomial R) (a : R) :
   root_multiplicity a p = if h0 : p = 0 then 0 else
   (multiplicity (X - C a) p).get (multiplicity_X_sub_C_finite a h0) :=
-by simp [multiplicity, root_multiplicity, roption.dom];
+by simp [multiplicity, root_multiplicity, part.dom];
   congr; funext; congr
 
 lemma pow_root_multiplicity_dvd (p : polynomial R) (a : R) :
diff --git a/src/data/rel.lean b/src/data/rel.lean
index 8204025ede594..3e0fa25444237 100644
--- a/src/data/rel.lean
+++ b/src/data/rel.lean
@@ -3,7 +3,7 @@ Copyright (c) 2018 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad
 -/
-import data.set.lattice
+import order.galois_connection
 
 /-!
 # Relations
diff --git a/src/order/omega_complete_partial_order.lean b/src/order/omega_complete_partial_order.lean
index dd70b69a64d11..b42c2def9d38a 100644
--- a/src/order/omega_complete_partial_order.lean
+++ b/src/order/omega_complete_partial_order.lean
@@ -27,7 +27,7 @@ supremum helps define the meaning of recursive procedures.
 
 ## Instances of `omega_complete_partial_order`
 
- * `roption`
+ * `part`
  * every `complete_lattice`
  * pi-types
  * product types
@@ -40,9 +40,9 @@ supremum helps define the meaning of recursive procedures.
    * `id`
    * `ite`
    * `const`
-   * `roption.bind`
-   * `roption.map`
-   * `roption.seq`
+   * `part.bind`
+   * `part.map`
+   * `part.seq`
 
 ## References
 
@@ -53,7 +53,7 @@ supremum helps define the meaning of recursive procedures.
 
 universes u v
 
-local attribute [-simp] roption.bind_eq_bind roption.map_eq_map
+local attribute [-simp] part.bind_eq_bind part.map_eq_map
 open_locale classical
 
 namespace preorder_hom
@@ -100,14 +100,14 @@ def prod.snd : (α × β) →ₘ β :=
 def prod.zip (f : α →ₘ β) (g : α →ₘ γ) : α →ₘ (β × γ) :=
 (prod.map f g).comp prod.diag
 
-/-- `roption.bind` as a monotone function -/
+/-- `part.bind` as a monotone function -/
 @[simps]
-def bind {β γ} (f : α →ₘ roption β) (g : α →ₘ β → roption γ) : α →ₘ roption γ :=
+def bind {β γ} (f : α →ₘ part β) (g : α →ₘ β → part γ) : α →ₘ part γ :=
 { to_fun := λ x, f x >>= g x,
   monotone' :=
   begin
     intros x y h a,
-    simp only [and_imp, exists_prop, roption.bind_eq_bind, roption.mem_bind_iff,
+    simp only [and_imp, exists_prop, part.bind_eq_bind, part.mem_bind_iff,
                exists_imp_distrib],
     intros b hb ha,
     refine ⟨b, f.monotone h _ hb, g.monotone h _ _ ha⟩,
@@ -309,12 +309,12 @@ end continuity
 
 end omega_complete_partial_order
 
-namespace roption
+namespace part
 
 variables {α : Type u} {β : Type v} {γ : Type*}
 open omega_complete_partial_order
 
-lemma eq_of_chain {c : chain (roption α)} {a b : α} (ha : some a ∈ c) (hb : some b ∈ c) : a = b :=
+lemma eq_of_chain {c : chain (part α)} {a b : α} (ha : some a ∈ c) (hb : some b ∈ c) : a = b :=
 begin
   cases ha with i ha, replace ha := ha.symm,
   cases hb with j hb, replace hb := hb.symm,
@@ -323,29 +323,29 @@ begin
   have := c.monotone h _ ha, apply mem_unique this hb
 end
 
-/-- The (noncomputable) `ωSup` definition for the `ω`-CPO structure on `roption α`. -/
-protected noncomputable def ωSup (c : chain (roption α)) : roption α :=
+/-- The (noncomputable) `ωSup` definition for the `ω`-CPO structure on `part α`. -/
+protected noncomputable def ωSup (c : chain (part α)) : part α :=
 if h : ∃a, some a ∈ c then some (classical.some h) else none
 
-lemma ωSup_eq_some {c : chain (roption α)} {a : α} (h : some a ∈ c) : roption.ωSup c = some a :=
+lemma ωSup_eq_some {c : chain (part α)} {a : α} (h : some a ∈ c) : part.ωSup c = some a :=
 have ∃a, some a ∈ c, from ⟨a, h⟩,
 have a' : some (classical.some this) ∈ c, from classical.some_spec this,
-calc roption.ωSup c = some (classical.some this) : dif_pos this
+calc part.ωSup c = some (classical.some this) : dif_pos this
                 ... = some a : congr_arg _ (eq_of_chain a' h)
 
-lemma ωSup_eq_none {c : chain (roption α)} (h : ¬∃a, some a ∈ c) : roption.ωSup c = none :=
+lemma ωSup_eq_none {c : chain (part α)} (h : ¬∃a, some a ∈ c) : part.ωSup c = none :=
 dif_neg h
 
-lemma mem_chain_of_mem_ωSup {c : chain (roption α)} {a : α} (h : a ∈ roption.ωSup c) : some a ∈ c :=
+lemma mem_chain_of_mem_ωSup {c : chain (part α)} {a : α} (h : a ∈ part.ωSup c) : some a ∈ c :=
 begin
-  simp [roption.ωSup] at h, split_ifs at h,
+  simp [part.ωSup] at h, split_ifs at h,
   { have h' := classical.some_spec h_1,
     rw ← eq_some_iff at h, rw ← h, exact h' },
   { rcases h with ⟨ ⟨ ⟩ ⟩ }
 end
 
-noncomputable instance omega_complete_partial_order : omega_complete_partial_order (roption α) :=
-{ ωSup    := roption.ωSup,
+noncomputable instance omega_complete_partial_order : omega_complete_partial_order (part α) :=
+{ ωSup    := part.ωSup,
   le_ωSup := λ c i, by { intros x hx, rw ← eq_some_iff at hx ⊢,
                          rw [ωSup_eq_some, ← hx], rw ← hx, exact ⟨i,rfl⟩ },
   ωSup_le := by { rintros c x hx a ha, replace ha := mem_chain_of_mem_ωSup ha,
@@ -353,9 +353,9 @@ noncomputable instance omega_complete_partial_order : omega_complete_partial_ord
 
 section inst
 
-lemma mem_ωSup (x : α) (c : chain (roption α)) : x ∈ ωSup c ↔ some x ∈ c :=
+lemma mem_ωSup (x : α) (c : chain (part α)) : x ∈ ωSup c ↔ some x ∈ c :=
 begin
-  simp [omega_complete_partial_order.ωSup,roption.ωSup],
+  simp [omega_complete_partial_order.ωSup,part.ωSup],
   split,
   { split_ifs, swap, rintro ⟨⟨⟩⟩,
     intro h', have hh := classical.some_spec h,
@@ -368,7 +368,7 @@ end
 
 end inst
 
-end roption
+end part
 
 namespace pi
 
@@ -613,26 +613,26 @@ lemma ite_continuous' {p : Prop} [hp : decidable p] (f g : α → β)
   (hf : continuous' f) (hg : continuous' g) : continuous' (λ x, if p then f x else g x) :=
 by split_ifs; simp *
 
-lemma ωSup_bind {β γ : Type v} (c : chain α) (f : α →ₘ roption β) (g : α →ₘ β → roption γ) :
+lemma ωSup_bind {β γ : Type v} (c : chain α) (f : α →ₘ part β) (g : α →ₘ β → part γ) :
   ωSup (c.map (f.bind g)) = ωSup (c.map f) >>= ωSup (c.map g) :=
 begin
   apply eq_of_forall_ge_iff, intro x,
-  simp only [ωSup_le_iff, roption.bind_le, chain.mem_map_iff, and_imp, preorder_hom.bind_coe,
+  simp only [ωSup_le_iff, part.bind_le, chain.mem_map_iff, and_imp, preorder_hom.bind_coe,
     exists_imp_distrib],
   split; intro h''',
   { intros b hb, apply ωSup_le _ _ _,
-    rintros i y hy, simp only [roption.mem_ωSup] at hb,
+    rintros i y hy, simp only [part.mem_ωSup] at hb,
     rcases hb with ⟨j,hb⟩, replace hb := hb.symm,
-    simp only [roption.eq_some_iff, chain.map_coe, function.comp_app, pi.monotone_apply_coe]
+    simp only [part.eq_some_iff, chain.map_coe, function.comp_app, pi.monotone_apply_coe]
       at hy hb,
     replace hb : b ∈ f (c (max i j))   := f.monotone (c.monotone (le_max_right i j)) _ hb,
     replace hy : y ∈ g (c (max i j)) b := g.monotone (c.monotone (le_max_left i j)) _ _ hy,
     apply h''' (max i j),
-    simp only [exists_prop, roption.bind_eq_bind, roption.mem_bind_iff, chain.map_coe,
+    simp only [exists_prop, part.bind_eq_bind, part.mem_bind_iff, chain.map_coe,
                function.comp_app, preorder_hom.bind_coe],
     exact ⟨_,hb,hy⟩, },
   { intros i, intros y hy,
-    simp only [exists_prop, roption.bind_eq_bind, roption.mem_bind_iff, chain.map_coe,
+    simp only [exists_prop, part.bind_eq_bind, part.mem_bind_iff, chain.map_coe,
                function.comp_app, preorder_hom.bind_coe] at hy,
     rcases hy with ⟨b,hb₀,hb₁⟩,
     apply h''' b _,
@@ -640,21 +640,21 @@ begin
     { apply le_ωSup (c.map f) i _ hb₀ } },
 end
 
-lemma bind_continuous' {β γ : Type v} (f : α → roption β) (g : α → β → roption γ) :
+lemma bind_continuous' {β γ : Type v} (f : α → part β) (g : α → β → part γ) :
   continuous' f → continuous' g →
   continuous' (λ x, f x >>= g x)
 | ⟨hf,hf'⟩ ⟨hg,hg'⟩ :=
 continuous.of_bundled' (preorder_hom.bind ⟨f,hf⟩ ⟨g,hg⟩)
   (by intro c; rw [ωSup_bind, ← hf', ← hg']; refl)
 
-lemma map_continuous' {β γ : Type v} (f : β → γ) (g : α → roption β)
+lemma map_continuous' {β γ : Type v} (f : β → γ) (g : α → part β)
   (hg : continuous' g) :
   continuous' (λ x, f <$> g x) :=
 by simp only [map_eq_bind_pure_comp];
    apply bind_continuous' _ _ hg;
    apply const_continuous'
 
-lemma seq_continuous' {β γ : Type v} (f : α → roption (β → γ)) (g : α → roption β)
+lemma seq_continuous' {β γ : Type v} (f : α → part (β → γ)) (g : α → part β)
   (hf : continuous' f) (hg : continuous' g) :
   continuous' (λ x, f x <*> g x) :=
 by simp only [seq_eq_bind_map];
@@ -807,28 +807,28 @@ def flip {α : Type*} (f : α → β →𝒄 γ) : β →𝒄 α → γ :=
   monotone' := λ x y h a, (f a).monotone h,
   cont := by intro; ext; change f x _ = _; rw [(f x).continuous ]; refl, }
 
-/-- `roption.bind` as a continuous function. -/
+/-- `part.bind` as a continuous function. -/
 @[simps { rhs_md := reducible }]
 noncomputable def bind {β γ : Type v}
-  (f : α →𝒄 roption β) (g : α →𝒄 β → roption γ) : α →𝒄 roption γ :=
+  (f : α →𝒄 part β) (g : α →𝒄 β → part γ) : α →𝒄 part γ :=
 of_mono (preorder_hom.bind (↑f) (↑g)) $ λ c, begin
   rw [preorder_hom.bind, ← preorder_hom.bind, ωSup_bind, ← f.continuous, ← g.continuous],
   refl
 end
 
-/-- `roption.map` as a continuous function. -/
+/-- `part.map` as a continuous function. -/
 @[simps {rhs_md := reducible}]
-noncomputable def map {β γ : Type v} (f : β → γ) (g : α →𝒄 roption β) : α →𝒄 roption γ :=
+noncomputable def map {β γ : Type v} (f : β → γ) (g : α →𝒄 part β) : α →𝒄 part γ :=
 of_fun (λ x, f <$> g x) (bind g (const (pure ∘ f))) $
 by ext; simp only [map_eq_bind_pure_comp, bind_to_fun, preorder_hom.bind_coe, const_apply,
   preorder_hom.const_coe, coe_apply]
 
-/-- `roption.seq` as a continuous function. -/
+/-- `part.seq` as a continuous function. -/
 @[simps {rhs_md := reducible}]
-noncomputable def seq {β γ : Type v} (f : α →𝒄 roption (β → γ)) (g : α →𝒄 roption β) :
-  α →𝒄 roption γ :=
+noncomputable def seq {β γ : Type v} (f : α →𝒄 part (β → γ)) (g : α →𝒄 part β) :
+  α →𝒄 part γ :=
 of_fun (λ x, f x <*> g x) (bind f $ (flip $ _root_.flip map g))
-  (by ext; simp only [seq_eq_bind_map, flip, roption.bind_eq_bind, map_to_fun, roption.mem_bind_iff,
+  (by ext; simp only [seq_eq_bind_map, flip, part.bind_eq_bind, map_to_fun, part.mem_bind_iff,
                       bind_to_fun, preorder_hom.bind_coe, coe_apply, flip_to_fun]; refl)
 
 end continuous_hom
diff --git a/src/ring_theory/multiplicity.lean b/src/ring_theory/multiplicity.lean
index ac0672d74fd20..cf6dac6cd95e5 100644
--- a/src/ring_theory/multiplicity.lean
+++ b/src/ring_theory/multiplicity.lean
@@ -23,7 +23,7 @@ several basic results on it.
 
 variables {α : Type*}
 
-open nat roption
+open nat part
 open_locale big_operators
 
 /-- `multiplicity a b` returns the largest natural number `n` such that
@@ -49,7 +49,7 @@ lemma finite_def {a b : α} : finite a b ↔ ∃ n : ℕ, ¬a ^ (n + 1) ∣ b :=
 theorem int.coe_nat_multiplicity (a b : ℕ) :
     multiplicity (a : ℤ) (b : ℤ) = multiplicity a b :=
 begin
-    apply roption.ext',
+    apply part.ext',
     { repeat {rw [← finite_iff_dom, finite_def]},
       norm_cast },
     { intros h1 h2,
@@ -146,7 +146,7 @@ lemma multiplicity_eq_zero_of_not_dvd {a b : α} (ha : ¬a ∣ b) : multiplicity
 eq_some_iff.2 (by simpa)
 
 lemma eq_top_iff_not_finite {a b : α} : multiplicity a b = ⊤ ↔ ¬ finite a b :=
-roption.eq_none_iff'
+part.eq_none_iff'
 
 lemma ne_top_iff_finite {a b : α} : multiplicity a b ≠ ⊤ ↔ finite a b :=
 by rw [ne.def, eq_top_iff_not_finite, not_not]
@@ -220,7 +220,7 @@ let ⟨n, hn⟩ := h in λ hb, by simpa [hb] using hn
 variable [decidable_rel ((∣) : α → α → Prop)]
 
 @[simp] protected lemma zero (a : α) : multiplicity a 0 = ⊤ :=
-roption.eq_none_iff.2 (λ n ⟨⟨k, hk⟩, _⟩, hk (dvd_zero _))
+part.eq_none_iff.2 (λ n ⟨⟨k, hk⟩, _⟩, hk (dvd_zero _))
 
 @[simp] lemma multiplicity_zero_eq_zero_of_ne_zero (a : α) (ha : a ≠ 0) : multiplicity 0 a = 0 :=
 begin
@@ -252,7 +252,7 @@ variables [comm_ring α] [decidable_rel ((∣) : α → α → Prop)]
 open_locale classical
 
 @[simp] protected lemma neg (a b : α) : multiplicity a (-b) = multiplicity a b :=
-roption.ext' (by simp only [multiplicity, enat.find, dvd_neg])
+part.ext' (by simp only [multiplicity, enat.find, dvd_neg])
   (λ h₁ h₂, enat.coe_inj.1 (by rw [enat.coe_get]; exact
     eq.symm (unique ((dvd_neg _ _).2 (pow_multiplicity_dvd _))
       (mt (dvd_neg _ _).1 (is_greatest' _ (lt_succ_self _))))))
@@ -342,7 +342,7 @@ eq_some_iff.2 ⟨by simp, λ ⟨b, hb⟩, ha (is_unit_iff_dvd_one.2
 
 @[simp] lemma get_multiplicity_self {a : α} (ha : finite a a) :
   get (multiplicity a a) ha = 1 :=
-roption.get_eq_iff_eq_some.2 (eq_some_iff.2
+part.get_eq_iff_eq_some.2 (eq_some_iff.2
   ⟨by simp, λ ⟨b, hb⟩,
     by rw [← mul_one a, pow_add, pow_one, mul_assoc, mul_assoc,
         mul_right_inj' (ne_zero_of_finite ha)] at hb;
diff --git a/test/general_recursion.lean b/test/general_recursion.lean
index ca29ed91a7ddf..587e1845c85b9 100644
--- a/test/general_recursion.lean
+++ b/test/general_recursion.lean
@@ -13,12 +13,12 @@ import data.nat.basic
 
 universes u_1 u_2
 
-namespace roption.examples
+namespace part.examples
 open function has_fix omega_complete_partial_order
 
 /-! `easy` is a trivial, non-recursive example -/
 
-def easy.intl (easy : ℕ → ℕ → roption ℕ) : ℕ → ℕ → roption ℕ
+def easy.intl (easy : ℕ → ℕ → part ℕ) : ℕ → ℕ → part ℕ
 | x y := pure x
 
 def easy :=
@@ -35,27 +35,27 @@ by rw [easy, lawful_fix.fix_eq' easy.cont]; refl
 
 /-! division on natural numbers -/
 
-def div.intl (div : ℕ → ℕ → roption ℕ) : ℕ → ℕ → roption ℕ
+def div.intl (div : ℕ → ℕ → part ℕ) : ℕ → ℕ → part ℕ
 | x y :=
 if y ≤ x ∧ y > 0
   then div (x - y) y
   else pure x
 
-def div : ℕ → ℕ → roption ℕ :=
+def div : ℕ → ℕ → part ℕ :=
 fix div.intl
 
 -- automation coming soon
 theorem div.cont : continuous' div.intl :=
 pi.omega_complete_partial_order.flip₂_continuous' div.intl
   (λ (x : ℕ),
-     pi.omega_complete_partial_order.flip₂_continuous' (λ (g : ℕ → ℕ → roption ℕ), div.intl g x)
+     pi.omega_complete_partial_order.flip₂_continuous' (λ (g : ℕ → ℕ → part ℕ), div.intl g x)
        (λ (x_1 : ℕ),
-            (continuous_hom.ite_continuous' (λ (x_2 : ℕ → ℕ → roption ℕ), x_2 (x - x_1) x_1)
-               (λ (x_1 : ℕ → ℕ → roption ℕ), pure x)
+            (continuous_hom.ite_continuous' (λ (x_2 : ℕ → ℕ → part ℕ), x_2 (x - x_1) x_1)
+               (λ (x_1 : ℕ → ℕ → part ℕ), pure x)
                (pi.omega_complete_partial_order.flip₁_continuous'
-                 (λ (v_1 : ℕ) (x_2 : ℕ → ℕ → roption ℕ), x_2 (x - x_1) v_1) _ $
+                 (λ (v_1 : ℕ) (x_2 : ℕ → ℕ → part ℕ), x_2 (x - x_1) v_1) _ $
                  pi.omega_complete_partial_order.flip₁_continuous'
-                   (λ (v : ℕ) (g : ℕ → ℕ → roption ℕ) (x : ℕ), g v x) _ id_continuous')
+                   (λ (v : ℕ) (g : ℕ → ℕ → part ℕ) (x : ℕ), g v x) _ id_continuous')
                (const_continuous' (pure x)))))
 
 -- automation coming soon
@@ -66,11 +66,11 @@ inductive tree (α : Type*)
 | nil {} : tree
 | node (x : α) : tree → tree → tree
 
-open roption.examples.tree
+open part.examples.tree
 
 /-! `map` on a `tree` using monadic notation -/
-def tree_map.intl {α β : Type*} (f : α → β) (tree_map : tree α → roption (tree β)) :
-  tree α → roption (tree β)
+def tree_map.intl {α β : Type*} (f : α → β) (tree_map : tree α → part (tree β)) :
+  tree α → part (tree β)
 | nil := pure nil
 | (node x t₀ t₁) :=
 do tt₀ ← tree_map t₀,
@@ -78,7 +78,7 @@ do tt₀ ← tree_map t₀,
    pure $ node (f x) tt₀ tt₁
 
 -- automation coming soon
-def tree_map {α : Type u_1} {β : Type u_2} (f : α → β) : tree α → roption (tree β) :=
+def tree_map {α : Type u_1} {β : Type u_2} (f : α → β) : tree α → part (tree β) :=
 fix (tree_map.intl f)
 
 -- automation coming soon
@@ -89,20 +89,20 @@ theorem tree_map.cont :
     (λ (x : tree α),
        tree.cases_on x (id (const_continuous' (pure nil)))
          (λ (x_x : α) (x_a x_a_1 : tree α),
-              (continuous_hom.bind_continuous' (λ (x : tree α → roption (tree β)), x x_a)
-                 (λ (x : tree α → roption (tree β)) (tt₀ : tree β),
+              (continuous_hom.bind_continuous' (λ (x : tree α → part (tree β)), x x_a)
+                 (λ (x : tree α → part (tree β)) (tt₀ : tree β),
                     x x_a_1 >>= λ (tt₁ : tree β), pure (node (f x_x) tt₀ tt₁))
-                 (pi.omega_complete_partial_order.flip₁_continuous' (λ (v : tree α) (x : tree α → roption (tree β)), x v) x_a id_continuous')
+                 (pi.omega_complete_partial_order.flip₁_continuous' (λ (v : tree α) (x : tree α → part (tree β)), x v) x_a id_continuous')
                  (pi.omega_complete_partial_order.flip₂_continuous'
-                    (λ (x : tree α → roption (tree β)) (tt₀ : tree β),
+                    (λ (x : tree α → part (tree β)) (tt₀ : tree β),
                        x x_a_1 >>= λ (tt₁ : tree β), pure (node (f x_x) tt₀ tt₁))
                     (λ (x : tree β),
-                       continuous_hom.bind_continuous' (λ (x : tree α → roption (tree β)), x x_a_1)
-                         (λ (x_1 : tree α → roption (tree β)) (tt₁ : tree β), pure (node (f x_x) x tt₁))
-                         (pi.omega_complete_partial_order.flip₁_continuous' (λ (v : tree α) (x : tree α → roption (tree β)), x v) x_a_1
+                       continuous_hom.bind_continuous' (λ (x : tree α → part (tree β)), x x_a_1)
+                         (λ (x_1 : tree α → part (tree β)) (tt₁ : tree β), pure (node (f x_x) x tt₁))
+                         (pi.omega_complete_partial_order.flip₁_continuous' (λ (v : tree α) (x : tree α → part (tree β)), x v) x_a_1
                             id_continuous')
                          (pi.omega_complete_partial_order.flip₂_continuous'
-                            (λ (x_1 : tree α → roption (tree β)) (tt₁ : tree β), pure (node (f x_x) x tt₁))
+                            (λ (x_1 : tree α → part (tree β)) (tt₁ : tree β), pure (node (f x_x) x tt₁))
                             (λ (x_1 : tree β), const_continuous' (pure (node (f x_x) x x_1)))))))))
 
 -- automation coming soon
@@ -119,14 +119,14 @@ by conv_lhs { rw [tree_map,lawful_fix.fix_eq' (tree_map.cont f)] }; refl
 
 /-! `map` on a `tree` using applicative notation -/
 
-def tree_map'.intl {α β} (f : α → β) (tree_map : tree α → roption (tree β)) :
-  tree α → roption (tree β)
+def tree_map'.intl {α β} (f : α → β) (tree_map : tree α → part (tree β)) :
+  tree α → part (tree β)
 | nil := pure nil
 | (node x t₀ t₁) :=
 node (f x) <$> tree_map t₀ <*> tree_map t₁
 
 -- automation coming soon
-def tree_map' {α : Type u_1} {β : Type u_2} (f : α → β) : tree α → roption (tree β) :=
+def tree_map' {α : Type u_1} {β : Type u_2} (f : α → β) : tree α → part (tree β) :=
 fix (tree_map'.intl f)
 
 -- automation coming soon
@@ -137,11 +137,11 @@ theorem tree_map'.cont :
     (λ (x : tree α),
        tree.cases_on x (id (const_continuous' (pure nil)))
          (λ (x_x : α) (x_a x_a_1 : tree α),
-              (continuous_hom.seq_continuous' (λ (x : tree α → roption (tree β)), node (f x_x) <$> x x_a)
-                 (λ (x : tree α → roption (tree β)), x x_a_1)
-                 (continuous_hom.map_continuous' (node (f x_x)) (λ (x : tree α → roption (tree β)), x x_a)
-                    (pi.omega_complete_partial_order.flip₁_continuous' (λ (v : tree α) (x : tree α → roption (tree β)), x v) x_a id_continuous'))
-                 (pi.omega_complete_partial_order.flip₁_continuous' (λ (v : tree α) (x : tree α → roption (tree β)), x v) x_a_1 id_continuous'))))
+              (continuous_hom.seq_continuous' (λ (x : tree α → part (tree β)), node (f x_x) <$> x x_a)
+                 (λ (x : tree α → part (tree β)), x x_a_1)
+                 (continuous_hom.map_continuous' (node (f x_x)) (λ (x : tree α → part (tree β)), x x_a)
+                    (pi.omega_complete_partial_order.flip₁_continuous' (λ (v : tree α) (x : tree α → part (tree β)), x v) x_a id_continuous'))
+                 (pi.omega_complete_partial_order.flip₁_continuous' (λ (v : tree α) (x : tree α → part (tree β)), x v) x_a_1 id_continuous'))))
 
 -- automation coming soon
 theorem tree_map'.equations.eqn_1 {α : Type u_1} {β : Type u_2} (f : α → β) :
@@ -158,25 +158,25 @@ ordering of its arguments and does not use the usual well-founded order
 on natural numbers. It is an interesting candidate to show that `fix` lets us disentangle
 the issue of termination from the definition of the function. -/
 
-def f91.intl (f91 : ℕ → roption ℕ) (n : ℕ) : roption ℕ :=
+def f91.intl (f91 : ℕ → part ℕ) (n : ℕ) : part ℕ :=
 if n > 100
   then pure $ n - 10
   else f91 (n + 11) >>= f91
 
 -- automation coming soon
-def f91 : ℕ → roption ℕ := fix f91.intl
+def f91 : ℕ → part ℕ := fix f91.intl
 
 -- automation coming soon
 lemma f91.cont : continuous' f91.intl :=
 pi.omega_complete_partial_order.flip₂_continuous' f91.intl
   (λ (x : ℕ),
      id
-       (continuous_hom.ite_continuous' (λ (x_1 : ℕ → roption ℕ), pure (x - 10)) (λ (x_1 : ℕ → roption ℕ), x_1 (x + 11) >>= x_1)
+       (continuous_hom.ite_continuous' (λ (x_1 : ℕ → part ℕ), pure (x - 10)) (λ (x_1 : ℕ → part ℕ), x_1 (x + 11) >>= x_1)
           (const_continuous' (pure (x - 10)))
-          (continuous_hom.bind_continuous' (λ (x_1 : ℕ → roption ℕ), x_1 (x + 11)) (λ (x : ℕ → roption ℕ), x)
-             (pi.omega_complete_partial_order.flip₁_continuous' (λ (v : ℕ) (x : ℕ → roption ℕ), x v) (x + 11) id_continuous')
-             (pi.omega_complete_partial_order.flip₂_continuous' (λ (x : ℕ → roption ℕ), x)
-                (λ (x_1 : ℕ), pi.omega_complete_partial_order.flip₁_continuous' (λ (v : ℕ) (g : ℕ → roption ℕ), g v) x_1 id_continuous')))))
+          (continuous_hom.bind_continuous' (λ (x_1 : ℕ → part ℕ), x_1 (x + 11)) (λ (x : ℕ → part ℕ), x)
+             (pi.omega_complete_partial_order.flip₁_continuous' (λ (v : ℕ) (x : ℕ → part ℕ), x v) (x + 11) id_continuous')
+             (pi.omega_complete_partial_order.flip₂_continuous' (λ (x : ℕ → part ℕ), x)
+                (λ (x_1 : ℕ), pi.omega_complete_partial_order.flip₁_continuous' (λ (v : ℕ) (g : ℕ → part ℕ), g v) x_1 id_continuous')))))
 .
 -- automation coming soon
 theorem f91.equations.eqn_1 (n : ℕ) : f91 n = ite (n > 100) (pure (n - 10)) (f91 (n + 11) >>= f91) :=
@@ -187,10 +187,10 @@ begin
   apply well_founded.induction (measure_wf $ λ n, 101 - n) n,
   clear n, dsimp [measure,inv_image], intros n ih,
   by_cases h' : n > 100,
-  { rw [roption.examples.f91.equations.eqn_1,if_pos h'],
+  { rw [part.examples.f91.equations.eqn_1,if_pos h'],
     existsi n - 10, rw nat.sub_add_eq_add_sub, norm_num [pure],
     apply le_of_lt, transitivity 100, norm_num, exact h' },
-  { rw [roption.examples.f91.equations.eqn_1,if_neg h'],
+  { rw [part.examples.f91.equations.eqn_1,if_neg h'],
     simp, rcases ih (n + 11) _ with ⟨n',hn₀,hn₁⟩,
     rcases ih (n') _ with ⟨n'',hn'₀,hn'₁⟩,
     refine ⟨n'',_,_,hn₁,hn'₁⟩,
@@ -200,7 +200,7 @@ begin
 end
 
 lemma f91_dom (n : ℕ) : (f91 n).dom :=
-by rw roption.dom_iff_mem; apply exists_imp_exists _ (f91_spec n); simp
+by rw part.dom_iff_mem; apply exists_imp_exists _ (f91_spec n); simp
 
 def f91' (n : ℕ) : ℕ := (f91 n).get (f91_dom n)
 
@@ -209,14 +209,14 @@ run_cmd guard (f91' 109 = 99)
 lemma f91_spec' (n : ℕ) : f91' n = if n > 100 then n - 10 else 91 :=
 begin
   suffices : (∃ n', n' ∈ f91 n ∧ n' = if n > 100 then n - 10 else 91),
-  { dsimp [f91'], rw roption.get_eq_of_mem,
+  { dsimp [f91'], rw part.get_eq_of_mem,
     rcases this with ⟨n,_,_⟩, subst n, assumption },
   apply well_founded.induction (measure_wf $ λ n, 101 - n) n,
   clear n, dsimp [measure,inv_image], intros n ih,
   by_cases h' : n > 100,
-  { rw [roption.examples.f91.equations.eqn_1,if_pos h',if_pos h'],
+  { rw [part.examples.f91.equations.eqn_1,if_pos h',if_pos h'],
     simp [pure] },
-  { rw [roption.examples.f91.equations.eqn_1,if_neg h',if_neg h'],
+  { rw [part.examples.f91.equations.eqn_1,if_neg h',if_neg h'],
     simp, rcases ih (n + 11) _ with ⟨n',hn'₀,hn'₁⟩,
     split_ifs at hn'₁,
     { subst hn'₁, norm_num at hn'₀, refine ⟨_,hn'₀,_⟩,
@@ -233,4 +233,4 @@ begin
     { clear ih, omega } }
 end
 
-end roption.examples
+end part.examples