Fixpoint type. There are still a few TODO for the non-expansiveness of sums,...
Fixpoint type. There are still a few TODO for the non-expansiveness of sums, products and functions.
Showing
- _CoqProject 1 addition, 0 deletions_CoqProject
- opam.pins 1 addition, 1 deletionopam.pins
- theories/lifetime/definitions.v 6 additions, 0 deletionstheories/lifetime/definitions.v
- theories/typing/bool.v 1 addition, 2 deletionstheories/typing/bool.v
- theories/typing/borrow.v 1 addition, 2 deletionstheories/typing/borrow.v
- theories/typing/fixpoint.v 67 additions, 0 deletionstheories/typing/fixpoint.v
- theories/typing/function.v 3 additions, 0 deletionstheories/typing/function.v
- theories/typing/own.v 11 additions, 1 deletiontheories/typing/own.v
- theories/typing/product.v 13 additions, 1 deletiontheories/typing/product.v
- theories/typing/shr_bor.v 11 additions, 3 deletionstheories/typing/shr_bor.v
- theories/typing/sum.v 3 additions, 0 deletionstheories/typing/sum.v
- theories/typing/type.v 142 additions, 2 deletionstheories/typing/type.v
- theories/typing/uninit.v 2 additions, 2 deletionstheories/typing/uninit.v
- theories/typing/uniq_bor.v 16 additions, 7 deletionstheories/typing/uniq_bor.v
Loading
Please register or sign in to comment