[Merged by Bors] - chore(data/set/basic): use decidable_pred (∈ s) instead of decidable_pred s.
#8211
Conversation
…le_pred s`. The latter exploits the fact that sets are functions to Prop, but this form is annoying as lemmas are never stated about it. In future we should consider removing the `set.decidable_mem` instance which encourages this misuse.
I've often wondered whether it would be better to make |
|
It looks like there's a bug either in the lean code for Edit: yep, the error originates from |
The downside of making set a structure is that |
This is neither alarming nor surprising. The SMT codebase hasn't been tested a lot, and finish is always a good way to make Lean segfault. See e.g. leanprover-community/lean#575 |
|
Do you think I should just eliminate the |
That's probably the easiest solution. |
eric-wieser
added
the
awaiting-review
Done |
|
bors r+ |
github-actions
bot
added
ready-to-merge
…le_pred s`. (#8211) The latter exploits the fact that sets are functions to Prop, and is an annoying form as lemmas are never stated about it. In future we should consider removing the `set.decidable_mem` instance which encourages this misuse. Making this change reveals a collection of pointless decidable arguments requiring that finset membership be decidable; something which is always true anyway. Two proofs in `data/pequiv` caused a crash inside the C++ portion of the `finish` tactic; it was easier to just write the simple proofs manually than to debug the C++ code.
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
decidable_pred (∈ s) instead of decidable_pred s.decidable_pred (∈ s) instead of decidable_pred s.
The only purpose of this instance was to enable the spelling `[decidable_pred s]` when what is actually needed is `decidable_pred (∈ s)`, which is a bad idea. This is a follow-up to #8211. Only two proofs needed this instance, and both were using completely the wrong lemmas anyway.
The latter exploits the fact that sets are functions to Prop, and is an annoying form as lemmas are never stated about it.
In future we should consider removing the
set.decidable_meminstance which encourages this misuse.Making this change reveals a collection of pointless decidable arguments requiring that finset membership be decidable; something which is always true anyway.
Two proofs in
data/pequivcaused a crash inside the C++ portion of thefinishtactic; it was easier to just write the simple proofs manually than to debug the C++ code.