Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
10
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Open sidebar
Marianna Rapoport
iris-coq
Commits
afb9d627
Commit
afb9d627
authored
Jun 08, 2018
by
Ralf Jung
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
convert Naming to markdown
parent
26827738
Changes
3
Hide whitespace changes
Inline
Side-by-side
Showing
3 changed files
with
86 additions
and
80 deletions
+86
-80
Naming.md
Naming.md
+84
-0
README.md
README.md
+2
-1
naming.txt
naming.txt
+0
-79
No files found.
Naming.md
0 → 100644
View file @
afb9d627
# Naming conventions for variables/arguments/hypotheses in the Coq development
## small letters
*
a : A = cmraT or cofeT
*
b : B = cmraT or cofeT
*
c
*
d
*
e : expr = expressions
*
f = some generic function
*
g = some generic function
*
h : heap
*
i
*
j
*
k
*
l
*
m : iGst = ghost state
*
n
*
o
*
p
*
q
*
r : iRes = resources
*
s = state (STSs)
*
s = stuckness bits
*
t
*
u
*
v : val = values of language
*
w
*
x
*
y
*
z
## capital letters
*
A : Type, cmraT or cofeT
*
B : Type, cmraT or cofeT
*
C
*
D
*
E : coPset = Viewshift masks
*
F = a functor
*
G
*
H = hypotheses
*
I = indexing sets
*
J
*
K : ectx = evaluation contexts
*
K = keys of a map
*
L
*
M = maps / global CMRA
*
N : namespace
*
O
*
P : uPred, iProp or Prop
*
Q : uPred, iProp or Prop
*
R : uPred, iProp or Prop
*
S : set state = state sets in STSs
*
T : set token = token sets in STSs
*
U
*
V : abstraction of value type in frame shift assertions
*
W
*
X : sets
*
Y : sets
*
Z : sets
## small greek letters
*
γ : gname
*
σ : state = state of language
*
φ : interpretation of STS/Auth
## capital greek letters
*
Φ : general predicate (over uPred, iProp or Prop)
*
Ψ : general predicate (over uPred, iProp or Prop)
# Naming conventions for algebraic classes in the Coq development
## Suffixes
*
T: canonical structurs (for example ofeT for OFEs, cmraT for cameras)
*
C: OFEs
*
R: cameras
*
UR: unital cameras or resources algebras
*
F: functors (can be combined with all of the above, e.g. CF is an OFE functor)
*
G: global camera functor management
README.md
View file @
afb9d627
...
...
@@ -81,7 +81,8 @@ followed by `make build-dep`.
document is
[
available online
](
http://plv.mpi-sws.org/iris/appendix-3.1.pdf
)
.
*
Information on how to set up your editor for unicode input and output is
collected in
[
Editor.md
](
Editor.md
)
.
*
The Iris Proof Mode (IPM) is documented at
[
ProofMode.md
](
ProofMode.md
)
*
The Iris Proof Mode (IPM) is documented at
[
ProofMode.md
](
ProofMode.md
)
.
*
Naming conventions are documented at
[
Naming.md
](
Naming.md
)
.
## Case Studies
...
...
naming.txt
deleted
100644 → 0
View file @
26827738
------------------ Naming conventions for variables/arguments/hypotheses in the Coq development ------------------
== small letters ==
a : A : cmraT or cofeT
b : B : cmraT or cofeT
c
d
e : expr = expressions
f : some generic function
g : some generic function
h : heap
i
j
k
l
m : iGst = ghost state
n
o
p
q
r : iRes = resources
s : state (STSs), stuckness bits
t
u
v : val = values of language
w
x
y
z
== capital letters ==
A : Type, cmraT or cofeT
B : Type, cmraT or cofeT
C
D
E : coPset = Viewshift masks
F : a functor
G
H : hypotheses
I : indexing sets
J
K : ectx = evaluation contexts
keys of a map
L
M : maps / global CMRA
N : namespace
O
P : uPred, iProp or Prop
Q : uPred, iProp or Prop
R : uPred, iProp or Prop
S : set state = state sets in STSs
T : set token = token sets in STSs
U
V : abstraction of value type in frame shift assertions
W
X : sets
Y : sets
Z : sets
== small greek letters ==
γ : gname
σ : state = state of language
φ : interpretation of STS/Auth
== capital greek letters ==
Φ : general predicate (over uPred, iProp or Prop)
Ψ : general predicate (over uPred, iProp or Prop)
------------------ Naming conventions for algebraic classes in the Coq development ------------------
== Suffixes ==
T: canonical structurs (for example ofeT for OFEs, cmraT for cameras)
C: OFEs
R: cameras
UR: unital cameras or resources algebras
F: functors (can be combined with all of the above, e.g. CF is an OFE functor)
G: global camera functor management
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment