Fix issue #206

When performing iDestruct ("H" with ...) as "#..." in the case that:

• H is in the spatial context, and,
• The BI is not affine

We cannot use the whole spatial context for both proving the premises of H and the resulting goal. As reported in #206 (closed), trying the above tactic currently gives an anomaly.

This MR issues this issue: Performing the above tactic will now consume the spatial premises.

TODO

This MR contains the following function that should be moved to std++:

Definition TC_to_bool (P : Prop)
  {p : bool} `{TCIf P (TCEq p true) (TCEq p false)} : boo

Given a proposition P that is a type class, it will return true if it can find an instance.

Any suggestions for a better name of this function?

Any suggestions for a better name of this function?

No strong opinion. TC_to_bool seems reasonable. Do we have other conversion-to-bool functions?

We have bool_decide, which turns a proposition into a Boolean provided it's decidable.

bool_of_class may be better then?

mentioned in merge request stdpp!48 (merged)

added 1 commit

• eacc2cf9 - Fix issue #206 (closed).

Compare with previous version

Updated this MR now that tc_to_bool is in stdpp.

resolved all discussions

merged

mentioned in commit 12db2bda