Open chdoc opened 4 years ago
This is bad indeed. For one part of my defense (FWIW) you are not supposed to unfold fsetI
;)
What happens next with !inE /=
is highly embarrassing...
I will look into this, thanks for pointing it out.
For one part of my defense (FWIW) you are not supposed to unfold
fsetI
;)
Yes, I realized that. Indeed, unfolding the defined operations can cause even more "funny" behaviors. I you replace &
with \
, then rewrite !inE /=
will rewrite the unfolded [fset x | x in A & x \notin B]
to (x \notin B) && (x \in A)
, presumably because it (still) uses the in_fsetD
rule rather than the in_fset
rule that one would expect to get from the printed goal. Ineed, rewriting with in_fset !inE /=
gives the expected [eta mem_seq ...]
mess. :unamused:
The following script showcases some unfortunate notation behaviors (on the current coq.dev and finmap.dev)