Commit 473e5f3c authored by David Swasey's avatar David Swasey

IrisRes no longer hides core resource and language types.

parent 0440ebb4
Require Import world_prop core_lang lang masks.
Require Import ModuRes.PCM ModuRes.UPred ModuRes.BI ModuRes.PreoMet ModuRes.Finmap.
Module IrisRes (RL : PCM_T) (C : CORE_LANG) <: PCM_T.
Import C.
Definition res := (pcm_res_ex state * RL.res)%type.
Module Type IRIS_RES (RL : PCM_T) (C : CORE_LANG) :=
PCM_T with Definition res := (pcm_res_ex C.state * RL.res)%type.
Module IrisRes (RL : PCM_T) (C : CORE_LANG) <: IRIS_RES RL C.
Definition res := (pcm_res_ex C.state * RL.res)%type.
Instance res_op : PCM_op res := _.
Instance res_unit : PCM_unit res := _.
Instance res_pcm : PCM res := _.
Markdown is supported
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