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
Iris
Iris
Commits
cbb493e7
Commit
cbb493e7
authored
Dec 07, 2017
by
Jacques-Henri Jourdan
Browse files
Remove useless comment.
parent
7678b4f9
Changes
1
Hide whitespace changes
Inline
Side-by-side
theories/base_logic/upred.v
View file @
cbb493e7
...
...
@@ -9,9 +9,6 @@ Set Default Proof Using "Type".
Record
uPred
(
M
:
ucmraT
)
:
Type
:
=
IProp
{
uPred_holds
:
>
nat
→
M
→
Prop
;
(* [uPred_mono] is used to prove non-expansiveness (guaranteed by
[uPred_ne]). Therefore, it is important that we do not restrict
it to only valid elements. *)
uPred_mono
n
x1
x2
:
uPred_holds
n
x1
→
x1
≼
{
n
}
x2
→
uPred_holds
n
x2
;
uPred_closed
n1
n2
x
:
uPred_holds
n1
x
→
n2
≤
n1
→
uPred_holds
n2
x
...
...
Write
Preview
Supports
Markdown
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