Skip to content
Projects
Groups
Snippets
Help
Loading...
Help
Support
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
C
coq-stdpp
Project overview
Project overview
Details
Activity
Releases
Cycle Analytics
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Charts
Issues
0
Issues
0
List
Boards
Labels
Milestones
Merge Requests
0
Merge Requests
0
CI / CD
CI / CD
Pipelines
Jobs
Schedules
Charts
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Charts
Create a new issue
Jobs
Commits
Issue Boards
Open sidebar
David Swasey
coq-stdpp
Commits
404f1473
Commit
404f1473
authored
Nov 16, 2015
by
Robbert Krebbers
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Setoid stuff for monadic operations.
parent
dcff8ded
Changes
2
Hide whitespace changes
Inline
Side-by-side
Showing
2 changed files
with
11 additions
and
11 deletions
+11
-11
theories/base.v
theories/base.v
+5
-5
theories/collections.v
theories/collections.v
+6
-6
No files found.
theories/base.v
View file @
404f1473
...
...
@@ -399,20 +399,20 @@ and fmap. We use these type classes merely for convenient overloading of
notations and do not formalize any theory on monads (we do not even define a
class with the monad laws). *)
Class
MRet
(
M
:
Type
→
Type
)
:
=
mret
:
∀
{
A
},
A
→
M
A
.
Instance
:
Params
(@
mret
)
3
.
Arguments
mret
{
_
_
_
}
_
.
Instance
:
Params
(@
mret
)
3
.
Class
MBind
(
M
:
Type
→
Type
)
:
=
mbind
:
∀
{
A
B
},
(
A
→
M
B
)
→
M
A
→
M
B
.
Arguments
mbind
{
_
_
_
_
}
_
!
_
/.
Instance
:
Params
(@
mbind
)
5
.
Instance
:
Params
(@
mbind
)
4
.
Class
MJoin
(
M
:
Type
→
Type
)
:
=
mjoin
:
∀
{
A
},
M
(
M
A
)
→
M
A
.
Instance
:
Params
(@
mjoin
)
3
.
Arguments
mjoin
{
_
_
_
}
!
_
/.
Instance
:
Params
(@
mjoin
)
3
.
Class
FMap
(
M
:
Type
→
Type
)
:
=
fmap
:
∀
{
A
B
},
(
A
→
B
)
→
M
A
→
M
B
.
Instance
:
Params
(@
fmap
)
6
.
Arguments
fmap
{
_
_
_
_
}
_
!
_
/.
Instance
:
Params
(@
fmap
)
4
.
Class
OMap
(
M
:
Type
→
Type
)
:
=
omap
:
∀
{
A
B
},
(
A
→
option
B
)
→
M
A
→
M
B
.
Instance
:
Params
(@
omap
)
6
.
Arguments
omap
{
_
_
_
_
}
_
!
_
/.
Instance
:
Params
(@
omap
)
4
.
Notation
"m ≫= f"
:
=
(
mbind
f
m
)
(
at
level
60
,
right
associativity
)
:
C_scope
.
Notation
"( m ≫=)"
:
=
(
λ
f
,
mbind
f
m
)
(
only
parsing
)
:
C_scope
.
...
...
theories/collections.v
View file @
404f1473
...
...
@@ -525,12 +525,12 @@ End fresh.
Section
collection_monad
.
Context
`
{
CollectionMonad
M
}.
Global
Instance
collection_fmap_proper
{
A
B
}
(
f
:
A
→
B
)
:
Proper
(
(
≡
)
==>
(
≡
))
(
fmap
f
).
Proof
.
intros
X
Y
[??]
;
split
;
esolve_elem_of
.
Qed
.
Global
Instance
collection_bind_proper
{
A
B
}
(
f
:
A
→
M
B
)
:
Proper
((
≡
)
==>
(
≡
))
(
mbind
f
).
Proof
.
intros
X
Y
[??]
;
split
;
esolve_elem_of
.
Qed
.
Global
Instance
collection_fmap_proper
{
A
B
}
:
Proper
(
pointwise_relation
_
(=)
==>
(
≡
)
==>
(
≡
))
(@
fmap
M
_
A
B
).
Proof
.
intros
f
g
?
X
Y
[??]
;
split
;
esolve_elem_of
.
Qed
.
Global
Instance
collection_bind_proper
{
A
B
}
:
Proper
((
(=)
==>
(
≡
))
==>
(
≡
)
==>
(
≡
))
(@
mbind
M
_
A
B
).
Proof
.
unfold
respectful
;
intros
f
g
Hfg
X
Y
[??]
;
split
;
esolve_elem_of
.
Qed
.
Global
Instance
collection_join_proper
{
A
}
:
Proper
((
≡
)
==>
(
≡
))
(@
mjoin
M
_
A
).
Proof
.
intros
X
Y
[??]
;
split
;
esolve_elem_of
.
Qed
.
...
...
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