Should it be a class (semantics/LTS/ReductionSystem)?

Stream: CSLib

[Fabrizio Montesi]

In semantics we currently tend to use definitions instead of classes, e.g.,

/-- An lts is image-finite if all images of its states are finite. -/
def LTS.ImageFinite : Prop :=
  ∀ s μ, Finite (lts.image s μ)

There are many similar general properties for LTS and reduction systems, for example the diamond property and confluence.

I wonder if these properties should be classes instead. Thoughts?

[Chris Henson]

If they produce something that is a typeclass like this, that seems reasonable.