From 81ab6978cc4230040a694e87604c809390da81ca Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 6 Jan 2017 21:31:33 +0100
Subject: [PATCH] Define the functors for the lifetime logic

---
 theories/lifetime/lifetime_sig.v | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v
index 3be29dd9..675899ed 100644
--- a/theories/lifetime/lifetime_sig.v
+++ b/theories/lifetime/lifetime_sig.v
@@ -56,7 +56,16 @@ Class lftPreG Σ := LftPreG {
   lft_preG_inh_inG :> inG Σ (authR inhUR);
 }.
 
-(* TODO: Write a Σ for lftPreG *)
+Definition lftΣ : gFunctors :=
+  #[ boxΣ; GFunctor (authR alftUR); GFunctor (authR ilftUR);
+     GFunctor (authR borUR); GFunctor (authR natUR); GFunctor (authR inhUR) ].
+Instance subG_stsΣ Σ :
+  subG lftΣ Σ → lftPreG Σ.
+Proof.
+  intros [? [?%subG_inG [?%subG_inG [?%subG_inG [?%subG_inG
+             ?%subG_inG]%subG_inv]%subG_inv]%subG_inv]%subG_inv]%subG_inv.
+  split; first apply _; done.
+Qed.
 
 Module Type lifetime_sig.
   (** Definitions *)
-- 
GitLab