Check whether variable exists

Stream: general

[Daniel Donnelly]

def object_instance_exists(self, o):
    pass

Hopefully o is a string

[Daniel Donnelly]

Part of my algorithm for connecting graphics items with Lean instances needs to check whether an object specified by o already exists. So how can we do that with Lean commands?

[Johan Commelin]

There is something like mk_fresh_name or something like that. I don't know anything about meta programming in Lean

[Daniel Donnelly]

@Johan Commelin thx, I'll look at my code again and see if I can use that instead

[Daniel Donnelly]

Can't really, unless I do a major redesign since I have:

[Daniel Donnelly]

def add_category(self, cat):
        if not self.interface().object_instance_exists(cat):
            self.interface().add_object_instance(cat)
        self.categories[id(cat)] = cat

[Daniel Donnelly]

Where interface() is the Lean interface

[Daniel Donnelly]

Shouldn't #check do the above?

[Daniel Donnelly]

I'll do some reading and figure out a way to make it work :)