Soundness of the type system. Also, added a file typing.v that reexports all the type system.
Showing
- _CoqProject 2 additions, 0 deletions_CoqProject
- opam.pins 1 addition, 1 deletionopam.pins
- theories/lang/tactics.v 1 addition, 1 deletiontheories/lang/tactics.v
- theories/lifetime/lifetime_sig.v 1 addition, 1 deletiontheories/lifetime/lifetime_sig.v
- theories/lifetime/model/definitions.v 1 addition, 1 deletiontheories/lifetime/model/definitions.v
- theories/typing/borrow.v 10 additions, 10 deletionstheories/typing/borrow.v
- theories/typing/fixpoint.v 1 addition, 0 deletionstheories/typing/fixpoint.v
- theories/typing/own.v 18 additions, 18 deletionstheories/typing/own.v
- theories/typing/product_split.v 13 additions, 13 deletionstheories/typing/product_split.v
- theories/typing/programs.v 0 additions, 1 deletiontheories/typing/programs.v
- theories/typing/soundness.v 78 additions, 0 deletionstheories/typing/soundness.v
- theories/typing/tests/get_x.v 1 addition, 4 deletionstheories/typing/tests/get_x.v
- theories/typing/tests/init_prod.v 2 additions, 5 deletionstheories/typing/tests/init_prod.v
- theories/typing/tests/lazy_lft.v 1 addition, 4 deletionstheories/typing/tests/lazy_lft.v
- theories/typing/tests/option_as_mut.v 1 addition, 4 deletionstheories/typing/tests/option_as_mut.v
- theories/typing/tests/rebor.v 1 addition, 4 deletionstheories/typing/tests/rebor.v
- theories/typing/tests/unbox.v 1 addition, 4 deletionstheories/typing/tests/unbox.v
- theories/typing/tests/unwrap_or.v 1 addition, 4 deletionstheories/typing/tests/unwrap_or.v
- theories/typing/type.v 1 addition, 1 deletiontheories/typing/type.v
- theories/typing/type_context.v 0 additions, 1 deletiontheories/typing/type_context.v
Loading
Please register or sign in to comment