在精益中，是否可以将decidable_linear_order与用户定义的相等关系一起使用？

Question

Lean附带了一个decidable_linear_order类型类，其中包含有关排序及其与相等的关系的有用引理，例如：

lemma eq_or_lt_of_not_lt [decidable_linear_order α] {a b : α} (h : ¬ a < b) : a = b ∨ b < a

这些排序中的等式都用=表示

inductive eq {α : Sort u} (a : α) : α → Prop
| refl : eq a

我想知道是否有可能以某种方式扩展这个类(及其超类)，以使用自反的、对称的和传递的、任意使用的已定义相等关系R: α → α → Prop，或者只有通过重写所有相关引理及其证明以使用R而不是eq才能实现

Answer 1

由于这些类不是由相等关系参数化的，因此您确实需要重新实现它们(也许元编程可能会对此有所帮助)。或者，因为您有一个等价关系，所以您可以在quotient类型上定义您的订单，因此继续使用eq。