Merge branch 'ci/ralf/ghostcell' into 'master'
add GhostCell proof See merge request iris/lambda-rust!19
Showing
- README.md 20 additions, 0 deletionsREADME.md
- _CoqProject 4 additions, 1 deletion_CoqProject
- theories/lang/notation.v 3 additions, 1 deletiontheories/lang/notation.v
- theories/lifetime/lifetime.v 71 additions, 0 deletionstheories/lifetime/lifetime.v
- theories/lifetime/lifetime_sig.v 20 additions, 7 deletionstheories/lifetime/lifetime_sig.v
- theories/lifetime/meta.v 67 additions, 0 deletionstheories/lifetime/meta.v
- theories/lifetime/model/creation.v 10 additions, 7 deletionstheories/lifetime/model/creation.v
- theories/lifetime/model/definitions.v 9 additions, 0 deletionstheories/lifetime/model/definitions.v
- theories/lifetime/model/primitive.v 7 additions, 0 deletionstheories/lifetime/model/primitive.v
- theories/typing/bool.v 2 additions, 2 deletionstheories/typing/bool.v
- theories/typing/borrow.v 24 additions, 14 deletionstheories/typing/borrow.v
- theories/typing/cont.v 5 additions, 3 deletionstheories/typing/cont.v
- theories/typing/cont_context.v 23 additions, 21 deletionstheories/typing/cont_context.v
- theories/typing/examples/nonlexical.v 10 additions, 1 deletiontheories/typing/examples/nonlexical.v
- theories/typing/fixpoint.v 1 addition, 1 deletiontheories/typing/fixpoint.v
- theories/typing/function.v 55 additions, 41 deletionstheories/typing/function.v
- theories/typing/int.v 4 additions, 4 deletionstheories/typing/int.v
- theories/typing/lft_contexts.v 178 additions, 83 deletionstheories/typing/lft_contexts.v
- theories/typing/lib/arc.v 17 additions, 17 deletionstheories/typing/lib/arc.v
- theories/typing/lib/brandedvec.v 418 additions, 0 deletionstheories/typing/lib/brandedvec.v
Loading
Please register or sign in to comment