Commit 2024-07-09 14:51 64a22263
View on Github →chore(Data/Set): golf and add decidability of insert (#14529)
Adds the insert version, golfs existing versions using inferInstanceAs.
Makes the lemmas all consistent about using Decidable vs DecidablePred.
These decidability instances are useful in downstream applications.