Skip to content
Projects
Groups
Snippets
Help
Loading...
Help
Contribute to GitLab
Sign in
Toggle navigation
C
cpdt
Project
Project
Details
Activity
Cycle Analytics
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Charts
Issues
0
Issues
0
List
Board
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
research
cpdt
Commits
0b0da1fa
Commit
0b0da1fa
authored
Oct 12, 2008
by
Adam Chlipala
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
s/stream/tree
parent
7230d443
Changes
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
with
2 additions
and
2 deletions
+2
-2
Coinductive.v
src/Coinductive.v
+2
-2
No files found.
src/Coinductive.v
View file @
0b0da1fa
...
...
@@ -465,8 +465,8 @@ Print constFold_ok.
%
\
item
%
#
<
li
>
#
Define
a
co
-
inductive
type
of
infinite
trees
carrying
data
of
a
fixed
parameter
type
.
Each
node
should
contain
a
data
value
and
two
child
trees
.
#
</
li
>
#
%
\
item
%
#
<
li
>
#
Define
a
function
[
everywhere
]
for
building
a
tree
with
the
same
data
value
at
every
node
.
#
</
li
>
#
%
\
item
%
#
<
li
>
#
Define
a
function
[
map
]
for
building
an
output
tree
out
of
two
input
trees
by
traversing
them
in
parallel
and
applying
a
two
-
argument
function
to
their
corresponding
data
values
.
#
</
li
>
#
%
\
item
%
#
<
li
>
#
Define
a
stream
[
falses
]
where
every
node
has
the
value
[
false
]
.
#
</
li
>
#
%
\
item
%
#
<
li
>
#
Define
a
stream
[
true_false
]
where
the
root
node
has
value
[
true
]
,
its
children
have
value
[
false
]
,
all
nodes
at
the
next
have
the
value
[
true
]
,
and
so
on
,
alternating
boolean
values
from
level
to
level
.
#
</
li
>
#
%
\
item
%
#
<
li
>
#
Define
a
tree
[
falses
]
where
every
node
has
the
value
[
false
]
.
#
</
li
>
#
%
\
item
%
#
<
li
>
#
Define
a
tree
[
true_false
]
where
the
root
node
has
value
[
true
]
,
its
children
have
value
[
false
]
,
all
nodes
at
the
next
have
the
value
[
true
]
,
and
so
on
,
alternating
boolean
values
from
level
to
level
.
#
</
li
>
#
%
\
item
%
#
<
li
>
#
Prove
that
[
true_falses
]
is
equal
to
the
result
of
mapping
the
boolean
"or"
function
[
orb
]
over
[
true_false
]
and
[
falses
]
.
You
can
make
[
orb
]
available
with
[
Require
Import
Bool
.
]
.
You
may
find
the
lemma
[
orb_false_r
]
from
the
same
module
helpful
.
Your
proof
here
should
not
be
about
the
standard
equality
[
=
]
,
but
rather
about
some
new
equality
relation
that
you
define
.
#
</
li
>
#
#
</
ol
>
#
%
\
end
{
enumerate
}%
#
</
li
>
#
...
...
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