Skip to content
Snippets Groups Projects
Commit d18e1bc6 authored by Yusuke Matsushita's avatar Yusuke Matsushita
Browse files

Update README.md

parent a0667458
No related branches found
No related tags found
No related merge requests found
Pipeline #65079 passed
Stage: build
Hide whitespace changes
Inline Side-by-side
Showing
with 8 additions and 2 deletions
README.md
+ 8
− 2
View file @ d18e1bc6
...@@ -31,14 +31,20 @@ followed by `make build-dep`. ...@@ -31,14 +31,20 @@ followed by `make build-dep`.
## Walkthrough ## Walkthrough
We have a [walkthrough](walkthrough.md) of RustHornBelt's Coq mechanization. We have a walkthrough ([walkthrough.md](walkthrough.md)) of RustHornBelt's Coq
development.
It explains in detail how to verify integer addition, model `Vec`, verify It explains in detail how to verify integer addition, model `Vec`, verify
`Vec::new`, and verify `mem::swap` (featuring mutable borrows). `Vec::new`, and verify `mem::swap` (featuring mutable borrows).
It focuses on the things you need to know to extend our Coq mechanization.
It is intended as a hands-on guide to our (huge) Coq development.
In particular, it focuses on the things you need to know to reuse and extend
the Coq development.
## Structure ## Structure
The [theories](theories) folder, which contains the Coq mechanization,
is structured as follows.
- The folder [util](theories/util) contains utility for basic concepts. - The folder [util](theories/util) contains utility for basic concepts.
- [fancy_lists.v](theories/util/fancy_lists.v) contains definitions, notation - [fancy_lists.v](theories/util/fancy_lists.v) contains definitions, notation
and lemmas for heterogeneous lists and related data types. and lemmas for heterogeneous lists and related data types.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment