Commit 2023-06-24 01:01 ceb42c50
View on Github →chore: remove legacy termination_by'
(#5426)
This adds a couple of WellFoundedRelation
instances, like for example WellFoundedRelation (WithBot Nat)
. Longer-term, we should probably add a WellFoundedOrder
class for types with a well-founded less-than relation and a [WellFoundOrder α] : WellFoundedRelation α
instance (or maybe just [LT α] [IsWellFounded fun a b : α => a < b] : WellFoundedRelation α
).