There was a problem fetching the pipeline mini graph.
Sharing (coercing uniq borrows to shared ones in the type system.
I also changed the spec : this can be done even if the lifetime is not ongoing, and thus it does not need tokens.
Showing
- theories/lifetime/borrow.v 2 additions, 2 deletionstheories/lifetime/borrow.v
- theories/lifetime/derived.v 11 additions, 2 deletionstheories/lifetime/derived.v
- theories/lifetime/frac_borrow.v 8 additions, 2 deletionstheories/lifetime/frac_borrow.v
- theories/lifetime/shr_borrow.v 5 additions, 0 deletionstheories/lifetime/shr_borrow.v
- theories/typing/function.v 11 additions, 9 deletionstheories/typing/function.v
- theories/typing/own.v 31 additions, 30 deletionstheories/typing/own.v
- theories/typing/perm.v 1 addition, 1 deletiontheories/typing/perm.v
- theories/typing/product.v 3 additions, 4 deletionstheories/typing/product.v
- theories/typing/shr_bor.v 35 additions, 30 deletionstheories/typing/shr_bor.v
- theories/typing/sum.v 6 additions, 19 deletionstheories/typing/sum.v
- theories/typing/type.v 26 additions, 20 deletionstheories/typing/type.v
- theories/typing/type_context.v 2 additions, 2 deletionstheories/typing/type_context.v
- theories/typing/uniq_bor.v 33 additions, 34 deletionstheories/typing/uniq_bor.v
Loading
Please register or sign in to comment