Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Dan Frumin
iris-coq
Commits
d7cae999
Commit
d7cae999
authored
Mar 09, 2016
by
Ralf Jung
Browse files
docs: update iris.sty
parent
21ad2d96
Changes
2
Hide whitespace changes
Inline
Side-by-side
docs/constructions.tex
View file @
d7cae999
...
...
@@ -6,7 +6,7 @@
Given some COFE
$
\cofe
$
, we define
$
\agm
(
\cofe
)
$
as follows:
\begin{align*}
\monoid
\eqdef
{}&
\setComp
{
(c, V)
\
subseteq
(
\mathbb
{
N
}
\to
T)
\times
\mathbb
{
N
}}{
\All
n, m. n
\geq
m
\Ra
n
\in
V
\Ra
m
\in
V
}
\\
\monoid
\eqdef
{}&
\setComp
{
(c, V)
\
in
(
\mathbb
{
N
}
\to
T)
\times
\pset
{
\mathbb
{
N
}}
}
{
\All
n, m. n
\geq
m
\Ra
n
\in
V
\Ra
m
\in
V
}
\\
&
\text
{
quotiented by
}
\\
(c
_
1, V
_
1)
\equiv
(c
_
1, V
_
2)
\eqdef
{}&
V
_
1 = V
_
2
\land
\All
n. n
\in
V
_
1
\Ra
c
_
1(n)
\nequiv
{
n
}
c
_
2(n)
\\
(c
_
1, V
_
1)
\nequiv
{
n
}
(c
_
1, V
_
2)
\eqdef
{}&
(
\All
m
\leq
n. m
\in
V
_
1
\Lra
m
\in
V
_
2)
\land
(
\All
m
\leq
n. m
\in
V
_
1
\Ra
c
_
1(m)
\nequiv
{
m
}
c
_
2(m))
\\
...
...
docs/iris.sty
View file @
d7cae999
...
...
@@ -106,10 +106,12 @@
%% Some commonly used identifiers
\newcommand
{
\SProp
}{
\textdom
{
SProp
}}
\newcommand
{
\UPred
}{
\textdom
{
UPred
}}
\newcommand
{
\mProp
}{
\textdom
{
Prop
}}
% meta-level prop
\newcommand
{
\iProp
}{
\textdom
{
iProp
}}
\newcommand
{
\Wld
}{
\textdom
{
Wld
}}
\newcommand
{
\Res
}{
\textdom
{
Res
}}
\newcommand
{
\cofe
}{
T
}
\newcommand
{
\cofeB
}{
U
}
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new 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