Zulip Chat Archive
Stream: new members
Topic: Using object of class inside other object of the same class?
Rick Overmeer (Apr 02 2024 at 13:45):
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 (Apr 02 2024 at 18:28):
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
Last updated: May 02 2025 at 03:31 UTC