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
e70a599d
Commit
e70a599d
authored
Sep 15, 2008
by
Adam Chlipala
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Make Chap. 3 title less grand
parent
e93229ac
Changes
2
Show whitespace changes
Inline
Side-by-side
Showing
2 changed files
with
2 additions
and
2 deletions
+2
-2
InductiveTypes.v
src/InductiveTypes.v
+1
-1
Intro.v
src/Intro.v
+1
-1
No files found.
src/InductiveTypes.v
View file @
e70a599d
...
@@ -16,7 +16,7 @@ Set Implicit Arguments.
...
@@ -16,7 +16,7 @@ Set Implicit Arguments.
(
*
end
hide
*
)
(
*
end
hide
*
)
(
**
%
\
chapter
{
Inductive
Types
}%
*
)
(
**
%
\
chapter
{
In
troducing
In
ductive
Types
}%
*
)
(
**
In
a
sense
,
CIC
is
built
from
just
two
relatively
straightforward
features
:
function
types
and
inductive
types
.
From
this
modest
foundation
,
we
can
prove
effectively
all
of
the
theorems
of
math
and
carry
out
effectively
all
program
verifications
,
with
enough
effort
expended
.
This
chapter
introduces
induction
and
recursion
in
Coq
and
shares
some
"design patterns"
for
overcoming
common
pitfalls
with
them
.
*
)
(
**
In
a
sense
,
CIC
is
built
from
just
two
relatively
straightforward
features
:
function
types
and
inductive
types
.
From
this
modest
foundation
,
we
can
prove
effectively
all
of
the
theorems
of
math
and
carry
out
effectively
all
program
verifications
,
with
enough
effort
expended
.
This
chapter
introduces
induction
and
recursion
in
Coq
and
shares
some
"design patterns"
for
overcoming
common
pitfalls
with
them
.
*
)
...
...
src/Intro.v
View file @
e70a599d
...
@@ -185,7 +185,7 @@ I believe that a good graphical interface to Coq is crucial for using it product
...
@@ -185,7 +185,7 @@ I believe that a good graphical interface to Coq is crucial for using it product
\
hline
\
hline
Some
Quick
Examples
&
\
texttt
{
StackMachine
.
v
}
\
\
Some
Quick
Examples
&
\
texttt
{
StackMachine
.
v
}
\
\
\
hline
\
hline
Inductive
Types
&
\
texttt
{
InductiveTypes
.
v
}
\
\
In
troducing
In
ductive
Types
&
\
texttt
{
InductiveTypes
.
v
}
\
\
\
hline
\
hline
\
end
{
tabular
}
\
end
{
center
}
\
end
{
tabular
}
\
end
{
center
}
...
...
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