Make uniform the naming of type classes over lists of types.

theories/typing/function.v

@@ -9,7 +9,7 @@ Section fn.
 
   Record fn_params := FP { fp_E : lft → elctx; fp_tys : vec type n; fp_ty : type }.
 
-  Definition FP_wf E (tys : vec type n) `{!TyWfLst tys} ty `{!TyWf ty} :=
+  Definition FP_wf E (tys : vec type n) `{!ListTyWf tys} ty `{!TyWf ty} :=
     FP (λ ϝ, E ϝ ++ tyl_wf_E tys ++ tyl_outlives_E tys ϝ ++
                     ty.(ty_wf_E) ++ ty_outlives_E ty ϝ)
        tys ty.

theories/typing/product.v

@@ -156,7 +156,7 @@ Section product.
   Definition product := foldr product2 unit0.
   Definition unit := product [].
 
-  Global Instance product_wf tyl `{!TyWfLst tyl} : TyWf (product tyl) :=
+  Global Instance product_wf tyl `{!ListTyWf tyl} : TyWf (product tyl) :=
     { ty_lfts := tyl_lfts tyl; ty_wf_E := tyl_wf_E tyl }.
 
   Lemma outlives_product ty1 ty2 ϝ `{!TyWf ty1, !TyWf ty2} :
@@ -179,11 +179,11 @@ Section product.
   Lemma product_proper' E L tyl1 tyl2 :
     Forall2 (eqtype E L) tyl1 tyl2 → eqtype E L (product tyl1) (product tyl2).
   Proof. apply product_proper. Qed.
-  Global Instance product_copy tys : LstCopy tys → Copy (product tys).
+  Global Instance product_copy tys : ListCopy tys → Copy (product tys).
   Proof. induction 1; apply _. Qed.
-  Global Instance product_send tys : LstSend tys → Send (product tys).
+  Global Instance product_send tys : ListSend tys → Send (product tys).
   Proof. induction 1; apply _. Qed.
-  Global Instance product_sync tys : LstSync tys → Sync (product tys).
+  Global Instance product_sync tys : ListSync tys → Sync (product tys).
   Proof. induction 1; apply _. Qed.
 
   Definition product_cons ty tyl :
@@ -252,7 +252,7 @@ Section typing.
     eqtype E L (Π[Π tyl1; Π tyl2]) (Π(tyl1 ++ tyl2)).
   Proof. by rewrite -prod_flatten_r -prod_flatten_l. Qed.
 
-  Lemma ty_outlives_E_elctx_sat_product E L tyl {Wf : TyWfLst tyl} α:
+  Lemma ty_outlives_E_elctx_sat_product E L tyl {Wf : ListTyWf tyl} α:
     elctx_sat E L (tyl_outlives_E tyl α) →
     elctx_sat E L (ty_outlives_E (Π tyl) α).
   Proof.

theories/typing/sum.v

@@ -84,7 +84,7 @@ Section sum.
     - iApply ((nth i tyl emp0).(ty_shr_mono) with "Hord"); done.
   Qed.
 
-  Global Instance sum_wf tyl `{!TyWfLst tyl} : TyWf (sum tyl) :=
+  Global Instance sum_wf tyl `{!ListTyWf tyl} : TyWf (sum tyl) :=
     { ty_lfts := tyl_lfts tyl; ty_wf_E := tyl_wf_E tyl }.
 
   Global Instance sum_type_ne n : Proper (Forall2 (type_dist2 n) ==> type_dist2 n) sum.
@@ -174,7 +174,7 @@ Section sum.
     nth i [] d = d.
   Proof. by destruct i. Qed.
 
-  Global Instance sum_copy tyl : LstCopy tyl → Copy (sum tyl).
+  Global Instance sum_copy tyl : ListCopy tyl → Copy (sum tyl).
   Proof.
     intros HFA. split.
     - intros tid vl.
@@ -215,7 +215,7 @@ Section sum.
         iMod ("Hclose" with "[$Hown1 $Hown2]") as "$". by iFrame.
   Qed.
 
-  Global Instance sum_send tyl : LstSend tyl → Send (sum tyl).
+  Global Instance sum_send tyl : ListSend tyl → Send (sum tyl).
   Proof.
     iIntros (Hsend tid1 tid2 vl) "H". iDestruct "H" as (i vl' vl'') "(% & % & Hown)".
     iExists _, _, _. iSplit; first done. iSplit; first done. iApply @send_change_tid; last done.
@@ -223,7 +223,7 @@ Section sum.
     iIntros (???) "[]".
   Qed.
 
-  Global Instance sum_sync tyl : LstSync tyl → Sync (sum tyl).
+  Global Instance sum_sync tyl : ListSync tyl → Sync (sum tyl).
   Proof.
     iIntros (Hsync κ tid1 tid2 l) "H". iDestruct "H" as (i) "[Hframe Hown]".
     iExists _. iFrame "Hframe". iApply @sync_change_tid; last done.

theories/typing/type.v

@@ -73,34 +73,34 @@ Proof.
 Qed.
 
 (* Lift TyWf to lists.  We cannot use `Forall` because that one is restricted to Prop. *)
-Inductive TyWfLst `{!typeG Σ} : list type → Type :=
-| tyl_wf_nil : TyWfLst []
-| tyl_wf_cons ty tyl `{!TyWf ty, !TyWfLst tyl} : TyWfLst (ty::tyl).
-Existing Class TyWfLst.
-Existing Instances tyl_wf_nil tyl_wf_cons.
+Inductive ListTyWf `{!typeG Σ} : list type → Type :=
+| list_ty_wf_nil : ListTyWf []
+| list_ty_wf_cons ty tyl `{!TyWf ty, !ListTyWf tyl} : ListTyWf (ty::tyl).
+Existing Class ListTyWf.
+Existing Instances list_ty_wf_nil list_ty_wf_cons.
 
-Fixpoint tyl_lfts `{!typeG Σ} tyl {WF : TyWfLst tyl} : list lft :=
+Fixpoint tyl_lfts `{!typeG Σ} tyl {WF : ListTyWf tyl} : list lft :=
   match WF with
-  | tyl_wf_nil => []
-  | tyl_wf_cons ty [] => ty.(ty_lfts)
-  | tyl_wf_cons ty tyl => ty.(ty_lfts) ++ tyl.(tyl_lfts)
+  | list_ty_wf_nil => []
+  | list_ty_wf_cons ty [] => ty.(ty_lfts)
+  | list_ty_wf_cons ty tyl => ty.(ty_lfts) ++ tyl.(tyl_lfts)
   end.
 
-Fixpoint tyl_wf_E `{!typeG Σ} tyl {WF : TyWfLst tyl} : elctx :=
+Fixpoint tyl_wf_E `{!typeG Σ} tyl {WF : ListTyWf tyl} : elctx :=
   match WF with
-  | tyl_wf_nil => []
-  | tyl_wf_cons ty [] => ty.(ty_wf_E)
-  | tyl_wf_cons ty tyl => ty.(ty_wf_E) ++ tyl.(tyl_wf_E)
+  | list_ty_wf_nil => []
+  | list_ty_wf_cons ty [] => ty.(ty_wf_E)
+  | list_ty_wf_cons ty tyl => ty.(ty_wf_E) ++ tyl.(tyl_wf_E)
   end.
 
-Fixpoint tyl_outlives_E `{!typeG Σ} tyl {WF : TyWfLst tyl} (κ : lft) : elctx :=
+Fixpoint tyl_outlives_E `{!typeG Σ} tyl {WF : ListTyWf tyl} (κ : lft) : elctx :=
   match WF with
-  | tyl_wf_nil => []
-  | tyl_wf_cons ty [] => ty_outlives_E ty κ
-  | tyl_wf_cons ty tyl => ty_outlives_E ty κ ++ tyl.(tyl_outlives_E) κ
+  | list_ty_wf_nil => []
+  | list_ty_wf_cons ty [] => ty_outlives_E ty κ
+  | list_ty_wf_cons ty tyl => ty_outlives_E ty κ ++ tyl.(tyl_outlives_E) κ
   end.
 
-Lemma tyl_outlives_E_elctx_sat `{!typeG Σ} E L tyl {WF : TyWfLst tyl} α β :
+Lemma tyl_outlives_E_elctx_sat `{!typeG Σ} E L tyl {WF : ListTyWf tyl} α β :
   tyl_outlives_E tyl β ⊆+ E →
   lctx_lft_incl E L α β →
   elctx_sat E L (tyl_outlives_E tyl α).
@@ -402,31 +402,31 @@ Class Copy `{!typeG Σ} (t : type) := {
 Existing Instances copy_persistent.
 Instance: Params (@Copy) 2 := {}.
 
-Class LstCopy `{!typeG Σ} (tys : list type) := lst_copy : Forall Copy tys.
-Instance: Params (@LstCopy) 2 := {}.
-Global Instance lst_copy_nil `{!typeG Σ} : LstCopy [] := List.Forall_nil _.
+Class ListCopy `{!typeG Σ} (tys : list type) := lst_copy : Forall Copy tys.
+Instance: Params (@ListCopy) 2 := {}.
+Global Instance lst_copy_nil `{!typeG Σ} : ListCopy [] := List.Forall_nil _.
 Global Instance lst_copy_cons `{!typeG Σ} ty tys :
-  Copy ty → LstCopy tys → LstCopy (ty :: tys) := List.Forall_cons _ _ _.
+  Copy ty → ListCopy tys → ListCopy (ty :: tys) := List.Forall_cons _ _ _.
 
 Class Send `{!typeG Σ} (t : type) :=
   send_change_tid tid1 tid2 vl : t.(ty_own) tid1 vl -∗ t.(ty_own) tid2 vl.
 Instance: Params (@Send) 2 := {}.
 
-Class LstSend `{!typeG Σ} (tys : list type) := lst_send : Forall Send tys.
-Instance: Params (@LstSend) 2 := {}.
-Global Instance lst_send_nil `{!typeG Σ} : LstSend [] := List.Forall_nil _.
+Class ListSend `{!typeG Σ} (tys : list type) := lst_send : Forall Send tys.
+Instance: Params (@ListSend) 2 := {}.
+Global Instance lst_send_nil `{!typeG Σ} : ListSend [] := List.Forall_nil _.
 Global Instance lst_send_cons `{!typeG Σ} ty tys :
-  Send ty → LstSend tys → LstSend (ty :: tys) := List.Forall_cons _ _ _.
+  Send ty → ListSend tys → ListSend (ty :: tys) := List.Forall_cons _ _ _.
 
 Class Sync `{!typeG Σ} (t : type) :=
   sync_change_tid κ tid1 tid2 l : t.(ty_shr) κ tid1 l -∗ t.(ty_shr) κ tid2 l.
 Instance: Params (@Sync) 2 := {}.
 
-Class LstSync `{!typeG Σ} (tys : list type) := lst_sync : Forall Sync tys.
-Instance: Params (@LstSync) 2 := {}.
-Global Instance lst_sync_nil `{!typeG Σ} : LstSync [] := List.Forall_nil _.
+Class ListSync `{!typeG Σ} (tys : list type) := lst_sync : Forall Sync tys.
+Instance: Params (@ListSync) 2 := {}.
+Global Instance lst_sync_nil `{!typeG Σ} : ListSync [] := List.Forall_nil _.
 Global Instance lst_sync_cons `{!typeG Σ} ty tys :
-  Sync ty → LstSync tys → LstSync (ty :: tys) := List.Forall_cons _ _ _.
+  Sync ty → ListSync tys → ListSync (ty :: tys) := List.Forall_cons _ _ _.
 
 Section type.
   Context `{!typeG Σ}.

theories/typing/type_sum.v

@@ -285,7 +285,7 @@ Section case.
     by iApply type_seq; [eapply type_sum_memcpy_instr, Hr|done|done].
   Qed.
 
-  Lemma ty_outlives_E_elctx_sat_sum E L tyl {Wf : TyWfLst tyl} α:
+  Lemma ty_outlives_E_elctx_sat_sum E L tyl {Wf : ListTyWf tyl} α:
     elctx_sat E L (tyl_outlives_E tyl α) →
     elctx_sat E L (ty_outlives_E (sum tyl) α).
   Proof.