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
Joshua Yanovski
iris-coq
Commits
69653240
Commit
69653240
authored
Mar 15, 2017
by
Robbert Krebbers
Browse files
Small tweaks.
parent
ea791308
Changes
1
Hide whitespace changes
Inline
Side-by-side
theories/base_logic/lib/fractional.v
View file @
69653240
...
...
@@ -131,14 +131,12 @@ Section fractional.
Ideally
,
it
'
d
not
even
be
possible
to
make
the
mistake
that
was
originally
made
here
,
which
is
to
give
this
instance
for
"false"
only
,
thus
breaking
some
intro
patterns
.
*
)
intros
H1
H2
H3
.
apply
mk_into_and_sep
.
rewrite
[
P
]
fractional_split
//.
intros
.
apply
mk_into_and_sep
.
rewrite
[
P
]
fractional_split
//.
Qed
.
Global
Instance
into_and_fractional_half
b
P
Q
Φ
q
:
AsFractional
P
Φ
q
→
AsFractional
Q
Φ
(
q
/
2
)
→
IntoAnd
b
P
Q
Q
|
100.
Proof
.
intros
H1
H2
.
apply
mk_into_and_sep
.
rewrite
[
P
]
fractional_half
//.
Qed
.
Proof
.
intros
.
apply
mk_into_and_sep
.
rewrite
[
P
]
fractional_half
//. Qed.
(
*
The
instance
[
frame_fractional
]
can
be
tried
at
all
the
nodes
of
the
proof
search
.
The
proof
search
then
fails
almost
always
on
...
...
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