Skip to content
Snippets Groups Projects
Commit 5e47e4ce authored by Ralf Jung's avatar Ralf Jung
Browse files

rename gen_heap_alloc_gen -> gen_heap_alloc_big

parent 7d2bf3fa
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
theories/base_logic/lib/gen_heap.v
+ 1
− 1
View file @ 5e47e4ce
...@@ -265,7 +265,7 @@ Section gen_heap. ...@@ -265,7 +265,7 @@ Section gen_heap.
rewrite !dom_insert_L. set_solver. rewrite !dom_insert_L. set_solver.
Qed. Qed.
Lemma gen_heap_alloc_gen σ σ' : Lemma gen_heap_alloc_big σ σ' :
σ' ##ₘ σ → σ' ##ₘ σ →
gen_heap_interp σ ==∗ gen_heap_interp σ ==∗
gen_heap_interp (σ' ∪ σ) ∗ ([∗ map] l ↦ v ∈ σ', l ↦ v) ∗ ([∗ map] l ↦ _ ∈ σ', meta_token l ⊤). gen_heap_interp (σ' ∪ σ) ∗ ([∗ map] l ↦ v ∈ σ', l ↦ v) ∗ ([∗ map] l ↦ _ ∈ σ', meta_token l ⊤).
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment