Using object of class inside other object of the same class?

Stream: new members

[Rick Overmeer]

Hi all,
I am pretty new to LEAN and was trying some things with classes and class instantiations. With this I was wondering if it is possible to use a function/object/element of a class instantiation (not sure of the correct wording in LEAN) inside another function/object/element of that same class instantiation. So to give an example I was wondering if we have the following code:

open Classical

class Schedule1 where
  jobs : Set Nat
  schedule: Nat -> Option Nat

def jobs_set : Set Nat := {0, 1}

noncomputable instance now1 : Schedule1 where
  jobs := jobs_set
  schedule j := if j ∈ jobs_set then some j else none

If it is possible to replace jobs_set inside schedule (and jobs) by jobs. So more concretely, if we can replace this piece of code by the following piece of code?

open Classical

class Schedule1 where
  jobs : Set Nat
  schedule: Nat -> Option Nat

noncomputable instance now1 : Schedule1 where
  jobs := {0, 1}
  schedule j := if j ∈ jobs then some j else none

I have not been able to find a way to do this in LEAN. Is there a way to do this I have not yet found? Or is this not possible in LEAN?

[Matt Diamond]

I think you may want to use structure instead of class here, and use def instead of instance... classes are useful when you have some type and you want to add structure to it, but there's no underlying type here