diff --git a/iris/bi/lib/fractional.v b/iris/bi/lib/fractional.v index 05dee6eeab90b4479539ed5c8335e4a0431b4aec..ac13b5f7966f79de2b6495d15dc1a7259fd7b701 100644 --- a/iris/bi/lib/fractional.v +++ b/iris/bi/lib/fractional.v @@ -14,9 +14,10 @@ Global Arguments AsFractional {_} _%I _%I _%Qp. Global Arguments fractional {_ _ _} _ _. -Global Hint Mode AsFractional - + - - : typeclass_instances. +Global Hint Mode AsFractional - ! - - : typeclass_instances. (* To make [as_fractional_fractional] a useful instance, we have to -allow [q] to be an evar. *) +allow [q] to be an evar. The head of [Φ] will always be a λ so ! is +not a useful mode there. *) Global Hint Mode AsFractional - - + - : typeclass_instances. Section fractional. diff --git a/tests/heap_lang.v b/tests/heap_lang.v index a83b6662da4ebea358c75f8b695bb7c5edd55a64..1c4d73212719176c83e45444075d63fb1581a3b3 100644 --- a/tests/heap_lang.v +++ b/tests/heap_lang.v @@ -368,6 +368,11 @@ Section mapsto_tests. iIntros (Φ) "Hl HΦ". Show. wp_load. by iApply "HΦ". Qed. + (* Make sure that we can split a mapsto containing an evar. *) + Lemma mapsto_evar_iSplit l v : + l ↦{#1 / 2} v -∗ ∃ q, l ↦{#1 / 2 + q} v. + Proof. iIntros "H". iExists _. iSplitL; first by iAssumption. Abort. + End mapsto_tests. Section inv_mapsto_tests.