Zulip Chat Archive

Stream: new members

Topic: Total orders on types

Henry Pearson (Jan 17 2022 at 11:34):

I'm trying to create AVL trees in lean and can't find code to force types to have a total order - this is necessary in order to create a well formed tree. Currently working on this function:

def insert (root : avlnode α) (ins_val : α) : avlnode α :=

but I need α to have a defined total order for this code to work.
If anyone knows how to do this would be very helpful!

Alex J. Best (Jan 17 2022 at 11:53):

docs#well_ordering_rel should be what you want

Anne Baanen (Jan 17 2022 at 11:55):

Alternatively, if the order is uniquely determined by α, you can write

def insert [linear_order α] (root : avlnode α) (ins_val : α) : avlnode α :=

and the < and operators will become available on α

Henry Pearson (Jan 17 2022 at 12:00):

Ah yeah that works - thanks a lot!

Last updated: Dec 20 2023 at 11:08 UTC