Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
7
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Open sidebar
Tej Chajed
iris
Commits
d19c06ae
Commit
d19c06ae
authored
Jan 26, 2017
by
Jacques-Henri Jourdan
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Typo.
parent
0c3914f7
Changes
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
with
2 additions
and
2 deletions
+2
-2
theories/algebra/csum.v
theories/algebra/csum.v
+2
-2
No files found.
theories/algebra/csum.v
View file @
d19c06ae
...
...
@@ -30,12 +30,12 @@ Implicit Types b : B.
(* Cofe *)
Inductive
csum_equiv
:
Equiv
(
csum
A
B
)
:
=
|
Cinl_equiv
a
a'
:
a
≡
a'
→
Cinl
a
≡
Cinl
a'
|
Cin
l
r_equiv
b
b'
:
b
≡
b'
→
Cinr
b
≡
Cinr
b'
|
Cinr_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'
|
Cin
l
r_dist
n
b
b'
:
b
≡
{
n
}
≡
b'
→
Cinr
b
≡
{
n
}
≡
Cinr
b'
|
Cinr_dist
n
b
b'
:
b
≡
{
n
}
≡
b'
→
Cinr
b
≡
{
n
}
≡
Cinr
b'
|
CsumBot_dist
n
:
CsumBot
≡
{
n
}
≡
CsumBot
.
Existing
Instance
csum_dist
.
...
...
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