Total orders on types

Stream: new members

[Henry Pearson]

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]

docs#well_ordering_rel should be what you want

[Anne Baanen]

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]

Ah yeah that works - thanks a lot!