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
Dan Frumin
iris-coq
Commits
c885513d
Commit
c885513d
authored
Jun 21, 2016
by
Robbert Krebbers
Browse files
Replace some non-unicode arrows.
parent
7e19e1e7
Changes
1
Hide whitespace changes
Inline
Side-by-side
algebra/csum.v
View file @
c885513d
...
...
@@ -8,8 +8,8 @@ Local Arguments cmra_validN _ _ !_ /.
Local
Arguments
cmra_valid
_
!
_
/
.
Inductive
csum
(
A
B
:
Type
)
:=
|
Cinl
:
A
->
csum
A
B
|
Cinr
:
B
->
csum
A
B
|
Cinl
:
A
→
csum
A
B
|
Cinr
:
B
→
csum
A
B
|
CsumBot
:
csum
A
B
.
Arguments
Cinl
{
_
_
}
_.
Arguments
Cinr
{
_
_
}
_.
...
...
@@ -22,13 +22,13 @@ Implicit Types b : B.
(
*
Cofe
*
)
Inductive
csum_equiv
:
Equiv
(
csum
A
B
)
:=
|
Cinl_equiv
a
a
'
:
a
≡
a
'
->
Cinl
a
≡
Cinl
a
'
|
Cinlr_equiv
b
b
'
:
b
≡
b
'
->
Cinr
b
≡
Cinr
b
'
|
Cinl_equiv
a
a
'
:
a
≡
a
'
→
Cinl
a
≡
Cinl
a
'
|
Cinlr_equiv
b
b
'
:
b
≡
b
'
→
Cinr
b
≡
Cinr
b
'
|
CsumBot_equiv
:
CsumBot
≡
CsumBot
.
Existing
Instance
csum_equiv
.
Inductive
csum_dist
:
Dist
(
csum
A
B
)
:=
|
Cinl_dist
n
a
a
'
:
a
≡
{
n
}
≡
a
'
->
Cinl
a
≡
{
n
}
≡
Cinl
a
'
|
Cinlr_dist
n
b
b
'
:
b
≡
{
n
}
≡
b
'
->
Cinr
b
≡
{
n
}
≡
Cinr
b
'
|
Cinl_dist
n
a
a
'
:
a
≡
{
n
}
≡
a
'
→
Cinl
a
≡
{
n
}
≡
Cinl
a
'
|
Cinlr_dist
n
b
b
'
:
b
≡
{
n
}
≡
b
'
→
Cinr
b
≡
{
n
}
≡
Cinr
b
'
|
CsumBot_dist
n
:
CsumBot
≡
{
n
}
≡
CsumBot
.
Existing
Instance
csum_dist
.
...
...
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