Commits · 65ced84b062e728fc743a08b5a4f2c76fbdfdc4b · Iris / lambda-rust

Mar 23, 2017
- subtyping for Rc · 65ced84b
  Ralf Jung authored 8 years ago
  
  65ced84b
- Rc is type contractive · cffd3c70
  Ralf Jung authored 8 years ago
  
  cffd3c70
- WIP. · 466fbcf0
  Jacques-Henri Jourdan authored 8 years ago
  
  466fbcf0
Mar 22, 2017
- fixed Rc, Cell · eeb2336d
  Ralf Jung authored 8 years ago
  
  eeb2336d
- WIP. · 823bd663
  Jacques-Henri Jourdan authored 8 years ago
  
  823bd663
- WIP. · 49951a90
  Jacques-Henri Jourdan authored 8 years ago
  
  49951a90
- WIP. · f851a9a0
  Jacques-Henri Jourdan authored 8 years ago
  
  f851a9a0
- fix spawn and cell · 69a91c8e
  Ralf Jung authored 8 years ago
  
  69a91c8e
- Add lemma [lctx_lft_alive_external], which is useful for automation. · dffd84ad
  Jacques-Henri Jourdan authored 8 years ago
  
  dffd84ad
- WIP work on option.v · 265b0b9c
  Ralf Jung authored 8 years ago
  
  265b0b9c
- WIP type_sum fixed · aa5a00a8
  Ralf Jung authored 8 years ago
  
  aa5a00a8
- Merge branch 'fnlft' of gitlab.mpi-sws.org:FP/LambdaRust-coq into fnlft · ff808bba
  Jacques-Henri Jourdan authored 8 years ago
  
  ff808bba
- WIP. · c4f2d1ee
  Jacques-Henri Jourdan authored 8 years ago
  
  c4f2d1ee
- WIP: new function rules done · dfb648ff
  Ralf Jung authored 8 years ago
  
  dfb648ff
- WIP sum: prove subtyping · 23b0aee0
  Ralf Jung authored 8 years ago
  
  23b0aee0
- WIP. · e6cb690a
  Jacques-Henri Jourdan authored 8 years ago
  
  e6cb690a
- WIP: "Lifetime of a function" instead of liveness assumptions in external lifetime context · de9fc5a6
  Ralf Jung authored 8 years ago
  
  de9fc5a6
Mar 16, 2017
- Remove 'Typeclasses Opaque' that were inside a section and hence ineffective · eaaec398
  Ralf Jung authored 8 years ago
  
  eaaec398
Mar 15, 2017
- Use `max_list_with` from std++. · c8636895
  Robbert Krebbers authored 8 years ago
  
  c8636895
- Update Iris. · 455be639
  Robbert Krebbers authored 8 years ago
  
  455be639
- Update to latest Iris. · 0df052f9
  Robbert Krebbers authored 8 years ago
  
  0df052f9
- Simplify a proof · 3f1d4314
  Ralf Jung authored 8 years ago
  
  3f1d4314
- Use new destruct for bigops · c5a967f0
  Ralf Jung authored 8 years ago
  
  c5a967f0
- update to latest Iris · b91fe227
  Ralf Jung authored 8 years ago
  
  b91fe227
- fix fallout of new bigops stuff in Iris · 07f64306
  Ralf Jung authored 8 years ago
  
  07f64306
- this should be right version of Iris · 2be5c7f4
  Ralf Jung authored 8 years ago
  
  2be5c7f4
- experiment with some lemmas to help reduce boilerplate in unsafe code proofs · a6cef604
  Ralf Jung authored 8 years ago
  
  a6cef604
- fix build · 4c4298f1
  Ralf Jung authored 8 years ago
  
  4c4298f1
- update Iris · 3a12bbe5
  Ralf Jung authored 8 years ago
  
  3a12bbe5
- proof script prettification · 8eb3580c
  Ralf Jung authored 8 years ago
  
  8eb3580c
Mar 14, 2017
- Update to latest Iris. · 7073b36a
  Robbert Krebbers authored 8 years ago
  
  7073b36a
Mar 13, 2017
- prove Rc::try_unwrap · 9e46ee7c
  Ralf Jung authored 8 years ago
  
  9e46ee7c
- add Rc::try_unwrap code · efa2ccbb
  Ralf Jung authored 8 years ago
  
  efa2ccbb
- Merge branch 'master' of https://gitlab.mpi-sws.org/FP/LambdaRust-coq · d30f6aa5
  Ralf Jung authored 8 years ago
  
  d30f6aa5
- change 'cont:' syntax to have explicit binder · 3953c673
  Ralf Jung authored 8 years ago
  
  3953c673
- Make type_jump easier to use by not having to give it the list of parameters. · e29c16ff
  Jacques-Henri Jourdan authored 8 years ago
  
  e29c16ff
- Prove weakening lemmas for elctx_sat. · 1076b6c9
  Jacques-Henri Jourdan authored 8 years ago
  
  1076b6c9
Mar 10, 2017
- note what is still missing for Rc · 91d84223
  Ralf Jung authored 8 years ago
  
  91d84223
- Rc::get_mut · 4f3ffcf2
  Ralf Jung authored 8 years ago
  
  4f3ffcf2
- make it so that we can give the option type (instead of the list of variants)... · 92bb9aaf
  Ralf Jung authored 8 years ago
  
  make it so that we can give the option type (instead of the list of variants) to the type_sum lemmas
  92bb9aaf