Skip to content

GitLab

Commit 1479da38 authored by Ralf Jung's avatar Ralf Jung
Browse files

mention lifetime equalization rule

parent 3a99ffb0
Pipeline #42828 passed with stage
in 20 minutes and 29 seconds
Hide whitespace changes
Inline Side-by-side
README.md
View file @ 1479da38
......@@ -38,6 +38,7 @@ Our Coq proof is based on the [RustBelt formalization](https://gitlab.mpi-sws.or
- The `BrandedVec` soundness proof is in [`theories/typing/lib/brandedvec.v`](theories/typing/lib/brandedvec.v).
- The `GhostCell` soundness proof is in [`theories/typing/lib/ghostcell.v`](theories/typing/lib/ghostcell.v).
- The new version of the "lifetime equalization" rule is `type_equivalize_lft` in [`theories/typing/programs.v`](theories/typing/programs.v).
## Prerequisites
......
Supports Markdown
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