Skip to content

Commit 5435910

Browse files
authored
fix: remove unnecessary noncomputable (#134)
`noncomputable` is not needed for the two instantiations.
1 parent f39bbcf commit 5435910

File tree

1 file changed

+2
-2
lines changed

1 file changed

+2
-2
lines changed

Cslib/Foundations/Semantics/LTS/Bisimulation.lean

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -235,11 +235,11 @@ section Order
235235

236236
/-! ## Order properties -/
237237

238-
noncomputable instance : Max {r // lts.IsBisimulation r} where
238+
instance : Max {r // lts.IsBisimulation r} where
239239
max r s := ⟨r.1 ⊔ s.1, Bisimulation.union r.2 s.2
240240

241241
/-- Bisimulations equipped with union form a join-semilattice. -/
242-
noncomputable instance : SemilatticeSup {r // lts.IsBisimulation r} where
242+
instance : SemilatticeSup {r // lts.IsBisimulation r} where
243243
sup r s := r ⊔ s
244244
le_sup_left r s := by
245245
simp only [LE.le]

0 commit comments

Comments
 (0)