Skip to content

GitLab

Switch branch/tag
Find file Normal viewHistoryPermalink
parameter.v 114 Bytes
Newer Older
Ralf Jung's avatar
(almost) instantiate lifting lemma for allocation  
Ralf Jung committed
1 2 3 
Require Export barrier.heap_lang.
Require Import iris.parameter.
Robbert Krebbers's avatar
Remove RA from the hierarchy.  
Robbert Krebbers committed
4 
Definition Σ := iParam_const heap_lang unitRA.