Lean4
instance : LinearOrder String where
le_refl _ := le_iff_toList_le.mpr le_rfl
le_trans a b
c := by
simp only [le_iff_toList_le]
apply le_trans
lt_iff_le_not_ge a b := by simp only [lt_iff_toList_lt, le_iff_toList_le, lt_iff_le_not_ge]
le_antisymm a
b := by
simp only [le_iff_toList_le, ← toList_inj]
apply le_antisymm
le_total a
b := by
simp only [le_iff_toList_le]
apply le_total
toDecidableLE := String.decidableLE
toDecidableEq := inferInstance
toDecidableLT := String.decidableLT'
compare_eq_compareOfLessAndEq a
b := by
simp only [compare, compareOfLessAndEq, instLT, List.instLT, lt_iff_toList_lt, toList]
split_ifs <;> simp only [List.lt_iff_lex_lt] at *
