make external lifetime context inclusion syntactic, and adjust type system and existing proofs
Showing
- README.md 20 additions, 0 deletionsREADME.md
- _CoqProject 1 addition, 1 deletion_CoqProject
- theories/lang/notation.v 1 addition, 1 deletiontheories/lang/notation.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 8 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/cell.v 9 additions, 9 deletionstheories/typing/lib/cell.v
- theories/typing/lib/diverging_static.v 38 additions, 15 deletionstheories/typing/lib/diverging_static.v
- theories/typing/lib/fake_shared.v 9 additions, 6 deletionstheories/typing/lib/fake_shared.v
- theories/typing/lib/join.v 2 additions, 2 deletionstheories/typing/lib/join.v
- theories/typing/lib/mutex/mutex.v 4 additions, 4 deletionstheories/typing/lib/mutex/mutex.v
- theories/typing/lib/mutex/mutexguard.v 19 additions, 16 deletionstheories/typing/lib/mutex/mutexguard.v
- theories/typing/lib/option.v 2 additions, 2 deletionstheories/typing/lib/option.v
Loading
Please register or sign in to comment