Adding more automation: extracting from a type context. Also, reformulated...
Adding more automation: extracting from a type context. Also, reformulated some of the proof rules, so that they can be applied without the consequence rule.
Showing
- theories/typing/bool.v 5 additions, 3 deletionstheories/typing/bool.v
- theories/typing/borrow.v 25 additions, 4 deletionstheories/typing/borrow.v
- theories/typing/case.v 31 additions, 2 deletionstheories/typing/case.v
- theories/typing/cont.v 1 addition, 1 deletiontheories/typing/cont.v
- theories/typing/function.v 28 additions, 12 deletionstheories/typing/function.v
- theories/typing/programs.v 24 additions, 8 deletionstheories/typing/programs.v
- theories/typing/type.v 6 additions, 7 deletionstheories/typing/type.v
- theories/typing/type_context.v 105 additions, 5 deletionstheories/typing/type_context.v
- theories/typing/uniq_bor.v 35 additions, 4 deletionstheories/typing/uniq_bor.v
Loading
Please register or sign in to comment