Expressed some instructions typing lemmas in terms of typed_body.
Showing
- opam.pins 1 addition, 1 deletionopam.pins
- theories/typing/borrow.v 6 additions, 2 deletionstheories/typing/borrow.v
- theories/typing/function.v 8 additions, 7 deletionstheories/typing/function.v
- theories/typing/own.v 39 additions, 29 deletionstheories/typing/own.v
- theories/typing/product_split.v 15 additions, 16 deletionstheories/typing/product_split.v
- theories/typing/programs.v 51 additions, 13 deletionstheories/typing/programs.v
- theories/typing/tests/get_x.v 4 additions, 12 deletionstheories/typing/tests/get_x.v
- theories/typing/type_context.v 5 additions, 0 deletionstheories/typing/type_context.v
- theories/typing/type_sum.v 9 additions, 10 deletionstheories/typing/type_sum.v
- theories/typing/uniq_bor.v 4 additions, 3 deletionstheories/typing/uniq_bor.v
Loading
Please register or sign in to comment