@[reducible]

def Auto.String.le (a b : String) : Prop

Equations

• Auto.String.le a b = (a = b ∨ a < b)

def Auto.String.lt (a b : String) : Prop

Equations

• Auto.String.lt a b = (a < b)