Mark gset methods as simpl never to stop `cbn` from unfolding them
This clarifies what's meant to happen anyway, and is apparently needed for cbn
. (I haven't yet tried doing this at the mapset
level).
Example of the problem: without this change, cbn
mangles the goal in the following:
Goal {[1; 2; 3]} =@{gset nat} ∅.
Fail progress simpl.
progress cbn. Show.
I'd want progress cbn
to fail, instead the above gives:
The command has indeed failed with message:
Failed to progress.
1 subgoal
============================
{| mapset_car := {[1 := ()]} ∪ {[2 := ()]} ∪ {[3 := ()]} |} = ∅