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
a71cf7dd
Commit
a71cf7dd
authored
9 years ago
by
Adam Chlipala
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Fix HTML filename convention
parent
ce3e5741
Changes
1
Show whitespace changes
Inline
Side-by-side
Showing
1 changed file
with
18 additions
and
18 deletions
+18
-18
toc.html
src/toc.html
+18
-18
No files found.
src/toc.html
View file @
a71cf7dd
...
...
@@ -4,23 +4,23 @@
<h1>
Certified Programming with Dependent Types
</h1>
<li><a
href=
"Intro.html"
>
Introduction
</a>
<li><a
href=
"StackMachine.html"
>
Some Quick Examples
</a>
<li><a
href=
"InductiveTypes.html"
>
Introducing Inductive Types
</a>
<li><a
href=
"Predicates.html"
>
Inductive Predicates
</a>
<li><a
href=
"Coinductive.html"
>
Infinite Data and Proofs
</a>
<li><a
href=
"Subset.html"
>
Subset Types and Variations
</a>
<li><a
href=
"GeneralRec.html"
>
General Recursion
</a>
<li><a
href=
"MoreDep.html"
>
More Dependent Types
</a>
<li><a
href=
"DataStruct.html"
>
Dependent Data Structures
</a>
<li><a
href=
"Equality.html"
>
Reasoning About Equality Proofs
</a>
<li><a
href=
"Generic.html"
>
Generic Programming
</a>
<li><a
href=
"Universes.html"
>
Universes and Axioms
</a>
<li><a
href=
"LogicProg.html"
>
Proof Search by Logic Programming
</a>
<li><a
href=
"Match.html"
>
Proof Search in Ltac
</a>
<li><a
href=
"Reflection.html"
>
Proof by Reflection
</a>
<li><a
href=
"Large.html"
>
Proving in the Large
</a>
<li><a
href=
"ProgLang.html"
>
A Taste of Reasoning About Programming Language Syntax
</a>
<li><a
href=
"Conclusion.html"
>
Conclusion
</a>
<li><a
href=
"
Cpdt.
Intro.html"
>
Introduction
</a>
<li><a
href=
"
Cpdt.
StackMachine.html"
>
Some Quick Examples
</a>
<li><a
href=
"
Cpdt.
InductiveTypes.html"
>
Introducing Inductive Types
</a>
<li><a
href=
"
Cpdt.
Predicates.html"
>
Inductive Predicates
</a>
<li><a
href=
"C
pdt.C
oinductive.html"
>
Infinite Data and Proofs
</a>
<li><a
href=
"
Cpdt.
Subset.html"
>
Subset Types and Variations
</a>
<li><a
href=
"
Cpdt.
GeneralRec.html"
>
General Recursion
</a>
<li><a
href=
"
Cpdt.
MoreDep.html"
>
More Dependent Types
</a>
<li><a
href=
"
Cpdt.
DataStruct.html"
>
Dependent Data Structures
</a>
<li><a
href=
"
Cpdt.
Equality.html"
>
Reasoning About Equality Proofs
</a>
<li><a
href=
"
Cpdt.
Generic.html"
>
Generic Programming
</a>
<li><a
href=
"
Cpdt.
Universes.html"
>
Universes and Axioms
</a>
<li><a
href=
"
Cpdt.
LogicProg.html"
>
Proof Search by Logic Programming
</a>
<li><a
href=
"
Cpdt.
Match.html"
>
Proof Search in Ltac
</a>
<li><a
href=
"
Cpdt.
Reflection.html"
>
Proof by Reflection
</a>
<li><a
href=
"
Cpdt.
Large.html"
>
Proving in the Large
</a>
<li><a
href=
"
Cpdt.
ProgLang.html"
>
A Taste of Reasoning About Programming Language Syntax
</a>
<li><a
href=
"C
pdt.C
onclusion.html"
>
Conclusion
</a>
</body></html>
This diff is collapsed.
Click to expand it.
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