Commit edfd4f51 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Rename sts -> stsT.

parent b7cf62fd
......@@ -7,7 +7,7 @@ Local Arguments unit _ _ !_ /.
Module sts.
Record Sts := {
Record stsT := STS {
state : Type;
token : Type;
trans : relation state;
......@@ -16,14 +16,14 @@ Record Sts := {
(* The type of bounds we can give to the state of an STS. This is the type
that we equip with an RA structure. *)
Inductive bound (sts : Sts) :=
Inductive bound (sts : stsT) :=
| bound_auth : state sts set (token sts) bound sts
| bound_frag : set (state sts) set (token sts ) bound sts.
Arguments bound_auth {_} _ _.
Arguments bound_frag {_} _ _.
Section sts_core.
Context (sts : Sts).
Context (sts : stsT).
Infix "≼" := dra_included.
Notation state := (state sts).
......@@ -239,7 +239,7 @@ Qed.
End sts_core.
Section stsRA.
Context (sts : Sts).
Context (sts : stsT).
Canonical Structure RA := validityRA (bound sts).
Definition auth (s : state sts) (T : set (token sts)) : RA :=
......@@ -299,7 +299,7 @@ Qed.
Lemma frag_included' S1 S2 T :
closed sts S2 T closed sts S1 T
S2 (S1 sts.up_set sts S2 )
S2 S1 sts.up_set sts S2
frag S1 T frag S2 T.
Proof.
intros. apply frag_included; first done.
......
......@@ -12,13 +12,13 @@ Module sts.
like you would use "auth_ctx" etc. *)
Export algebra.sts.sts.
Class InG Λ Σ (i : gid) (sts : Sts) := {
Class InG Λ Σ (i : gid) (sts : stsT) := {
inG :> ghost_ownership.InG Λ Σ i (sts.RA sts);
inh :> Inhabited (state sts);
}.
Section definitions.
Context {Λ Σ} (i : gid) (sts : Sts) `{!InG Λ Σ i sts} (γ : gname).
Context {Λ Σ} (i : gid) (sts : stsT) `{!InG Λ Σ i sts} (γ : gname).
Definition inv (φ : state sts iPropG Λ Σ) : iPropG Λ Σ :=
( s, own i γ (auth sts s ) φ s)%I.
Definition in_states (S : set (state sts)) (T: set (token sts)) : iPropG Λ Σ:=
......@@ -34,7 +34,7 @@ Instance: Params (@in_state) 6.
Instance: Params (@ctx) 7.
Section sts.
Context {Λ Σ} (i : gid) (sts : Sts) `{!InG Λ Σ StsI sts}.
Context {Λ Σ} (i : gid) (sts : stsT) `{!InG Λ Σ StsI sts}.
Context (φ : state sts iPropG Λ Σ).
Implicit Types N : namespace.
Implicit Types P Q R : iPropG Λ Σ.
......
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