From 7654e932f52e50b274f661139cfff6457792bb22 Mon Sep 17 00:00:00 2001
From: Xueying Qin <32066429+XYUnknown@users.noreply.github.com>
Date: Mon, 27 Oct 2025 17:29:39 +0000
Subject: [PATCH] remove noncomputable

---
 Cslib/Foundations/Semantics/LTS/Bisimulation.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Cslib/Foundations/Semantics/LTS/Bisimulation.lean b/Cslib/Foundations/Semantics/LTS/Bisimulation.lean
index 2abe2e93..2526d3f4 100644
--- a/Cslib/Foundations/Semantics/LTS/Bisimulation.lean
+++ b/Cslib/Foundations/Semantics/LTS/Bisimulation.lean
@@ -235,11 +235,11 @@ section Order
 
 /-! ## Order properties -/
 
-noncomputable instance : Max {r // lts.IsBisimulation r} where
+instance : Max {r // lts.IsBisimulation r} where
   max r s := ⟨r.1 ⊔ s.1, Bisimulation.union r.2 s.2⟩
 
 /-- Bisimulations equipped with union form a join-semilattice. -/
-noncomputable instance : SemilatticeSup {r // lts.IsBisimulation r} where
+instance : SemilatticeSup {r // lts.IsBisimulation r} where
   sup r s := r ⊔ s
   le_sup_left r s := by
     simp only [LE.le]