Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Janno
iris-coq
Commits
df120ac8
Commit
df120ac8
authored
Oct 22, 2016
by
Ralf Jung
Browse files
docs: add linkto website
parent
6cdc15f5
Changes
2
Hide whitespace changes
Inline
Side-by-side
docs/base-logic.tex
View file @
df120ac8
...
...
@@ -395,7 +395,7 @@ Furthermore, we have the usual $\eta$ and $\beta$ laws for projections, $\lambda
{
\ownM\melt
\proves
\upd
\Exists\meltB\in\meltsB
.
\ownM\meltB
}
\end{mathpar}
The premise in
\ruleref
{
upd-update
}
is a
\emph
{
meta-level
}
side-condition that has to be proven about
$
a
$
and
$
B
$
.
\ralf
{
Trouble is, we don't actually have
$
\in
$
inside the logic...
}
%
\ralf{Trouble is, we don't actually have $\in$ inside the logic...}
\subsection
{
Consistency
}
...
...
docs/iris.tex
View file @
df120ac8
...
...
@@ -18,7 +18,7 @@
\begin{document}
\title
{
\bfseries
The Iris 2.0 Documentation
}
%
\author{
The Iris Team
}
\author
{
\url
{
http://plv.mpi-sws.org/iris/
}
}
\maketitle
\thispagestyle
{
empty
}
...
...
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