在精益中，是否可以使用具有用户定义的相等关系的decidable_linear_order？

作者: 老人与海。
发布时间: 2025-01-19 02:52:19 (11天前)
转自：

2 条回复

0#
回复此人
⑩Ⅵ嵗Ｄ夨憶 | 2019-08-31 10-32

<div class =“post-text”itemprop =“text”> <P> 由于这些类没有通过等式关系参数化，你确实必须重新实现它们（也许元编程可能对此有所帮助）。或者，因为您有等价关系，您可以在商类型上定义您的订单，因此继续使用 <code> eq </code> 。 </p> </DIV>

编辑

登录后才能参与评论