Skip to content

Mark gset methods as simpl never to stop `cbn` from unfolding them

Paolo G. Giarrusso requested to merge Blaisorblade/stdpp:gset-simpl-never into master

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 := ()]} |} = ∅

Merge request reports

Loading