fix: computable KleeneAlgebra (Language α) instance (#3585)

This is another case of leanprover/lean4#2096
leanprover-community · Apr 22, 2023 · 754c3ef · 754c3ef
1 parent b53dd02
commit 754c3ef
Showing 1 changed file with 3 additions and 4 deletions.
diff --git a/Mathlib/Computability/Language.lean b/Mathlib/Computability/Language.lean
@@ -292,10 +292,9 @@ theorem one_add_kstar_mul_self_eq_kstar (l : Language α) : 1 + l∗ * l = l∗
   rw [mul_self_kstar_comm, one_add_self_mul_kstar_eq_kstar]
 #align language.one_add_kstar_mul_self_eq_kstar Language.one_add_kstar_mul_self_eq_kstar
 
--- Porting note: `noncomputable` required.
-noncomputable instance : KleeneAlgebra (Language α) :=
-  { Language.instSemiringLanguage, Set.instCompleteBooleanAlgebraSet,
-      Language.instKStarLanguage with
+instance : KleeneAlgebra (Language α) :=
+  { Language.instSemiringLanguage, Set.instCompleteBooleanAlgebraSet with
+    kstar := fun L ↦ L∗,
     one_le_kstar := fun a l hl ↦ ⟨[], hl, by simp⟩,
     mul_kstar_le_kstar := fun a ↦ (one_add_self_mul_kstar_eq_kstar a).le.trans' le_sup_right,
     kstar_mul_le_kstar := fun a ↦ (one_add_kstar_mul_self_eq_kstar a).le.trans' le_sup_right,