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
Iris
stdpp
Commits
4978faed
Commit
4978faed
authored
Jun 20, 2019
by
Robbert Krebbers
Browse files
Add `proj1_ex` and `proj2_ex` when ∃ over `Prop`.
parent
9d08f65f
Pipeline
#17818
passed with stage
in 10 minutes and 40 seconds
Changes
1
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
theories/base.v
View file @
4978faed
...
...
@@ -753,6 +753,10 @@ Section sig_map.
End
sig_map
.
Arguments
sig_map
_
_
_
_
_
_
!
_
/
:
assert
.
Definition
proj1_ex
{
P
:
Prop
}
{
Q
:
P
→
Prop
}
(
p
:
∃
x
,
Q
x
)
:
P
:
=
let
'
(
ex_intro
_
x
_
)
:
=
p
in
x
.
Definition
proj2_ex
{
P
:
Prop
}
{
Q
:
P
→
Prop
}
(
p
:
∃
x
,
Q
x
)
:
Q
(
proj1_ex
p
)
:
=
let
'
(
ex_intro
_
x
H
)
:
=
p
in
H
.
(** * Operations on sets *)
(** We define operational type classes for the traditional operations and
...
...
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