chore(real/cau_seq_completion): put class in Prop (#12533)

leanprover-community · Mar 9, 2022 · b8d176e · b8d176e
1 parent 1f6a2e9
commit b8d176e
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 3 deletions.
diff --git a/src/data/complex/basic.lean b/src/data/complex/basic.lean
@@ -661,7 +661,7 @@ theorem equiv_lim_aux (f : cau_seq ℂ abs) : f ≈ cau_seq.const abs (lim_aux f
   rwa add_halves at this,
 end
 
-noncomputable instance : cau_seq.is_complete ℂ abs :=
+instance : cau_seq.is_complete ℂ abs :=
 ⟨λ f, ⟨lim_aux f, equiv_lim_aux f⟩⟩
 
 open cau_seq

diff --git a/src/data/real/basic.lean b/src/data/real/basic.lean
@@ -569,6 +569,6 @@ begin
     exact ih _ ij }
 end
 
-noncomputable instance : cau_seq.is_complete ℝ abs := ⟨cau_seq_converges⟩
+instance : cau_seq.is_complete ℝ abs := ⟨cau_seq_converges⟩
 
 end real
diff --git a/src/data/real/cau_seq_completion.lean b/src/data/real/cau_seq_completion.lean
@@ -171,7 +171,7 @@ variables (β : Type*) [ring β] (abv : β → α) [is_absolute_value abv]
 
 /-- A class stating that a ring with an absolute value is complete, i.e. every Cauchy
 sequence has a limit. -/
-class is_complete :=
+class is_complete : Prop :=
 (is_complete : ∀ s : cau_seq β abv, ∃ b : β, s ≈ const abv b)
 end