Make [ELCtx_Alive] a coercion (!6) · Merge requests · Iris / lambda-rust · GitLab

Snippets Groups Projects

Merged Jacques-Henri Jourdan requested to merge jh/alive_coercions into master 8 years ago

Mar 06, 2017
- Notation FP' as a wrapper for FP, so that the arguments are in the right order. · 53d600fc
  Jacques-Henri Jourdan authored 8 years ago
  
  53d600fc
- Make the notation for function types work even if used with more than on variable. · 9ddb6194
  Jacques-Henri Jourdan authored 8 years ago and Jacques-Henri Jourdan committed 8 years ago
  
  This still does not work for parsing, because of a bug in Coq. But at least for printing this is OK, and this is ready for when we will switch to 8.6pl1.
  9ddb6194
- Make [ELCtx_Alive] a coercion. · 73fe10ef
  Jacques-Henri Jourdan authored 8 years ago and Jacques-Henri Jourdan committed 8 years ago
  
  I needed to uncurry the [fn] type, so that type inference infers first that the generalized variables are lifetimes, before typechecking the external lifetime contexts.
  73fe10ef
- Make [lft] an Opaque type, when seen from outside of the lifetime logic model. · 094097c8
  Jacques-Henri Jourdan authored 8 years ago and Jacques-Henri Jourdan committed 8 years ago
  
  This will make it possible to declare ELCtx_Alive a coercion.
  094097c8