Commit 82563700 by Dan Frumin

### a wee cleanup

parent 616906bb
 ... @@ -656,7 +656,7 @@ Section flock. ... @@ -656,7 +656,7 @@ Section flock. iDestruct (own_valid_2 with "Haprops HI") iDestruct (own_valid_2 with "Haprops HI") as %[Hfoo _]%auth_valid_discrete_2. as %[Hfoo _]%auth_valid_discrete_2. (* TODO: RK, please take a look at this horrific script *) (* TODO: RK, can this proof script be simplified? The idea is not complicated. *) (* We are going to separate the active resources I out of the fp map *) (* We are going to separate the active resources I out of the fp map *) pose (I'' := fmap res_name I). pose (I'' := fmap res_name I). assert (∃ P', P' ##ₘ I'' ∧ fp ≡ P' ∪ I'') as [P' HP']. assert (∃ P', P' ##ₘ I'' ∧ fp ≡ P' ∪ I'') as [P' HP']. ... ...
 ... @@ -36,7 +36,7 @@ Section tests_vcg. ... @@ -36,7 +36,7 @@ Section tests_vcg. intros. vcg. iExists (n). repeat iSplit; eauto. intros. vcg. iExists (n). repeat iSplit; eauto. { iPureIntro. lia. } { iPureIntro. lia. } iIntros (l) "? Hl". assert (∃ m, n = S m) as [k ->]. exists (pred n). lia. iIntros (l) "? Hl". assert (∃ m, n = S m) as [k ->]. exists (pred n). lia. iDestruct "Hl" as "[Hl Hls]". (* TODO: this looks ridiculous *) iDestruct "Hl" as "[Hl Hls]". vcg_continue. eauto 42 with iFrame. vcg_continue. eauto 42 with iFrame. Qed. Qed. ... ...
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!