Commits · b1e5b11ee1d35f8cdc6e937908e23fa84c73fa94 · Simon Spies / lambda-rust · GitLab

Snippets Groups Projects

Dec 21, 2016
- ssreflect 1.6.1 is out :) · b1e5b11e
  Ralf Jung authored 8 years ago
  
  b1e5b11e
- prove read_own_move · c6051ad0
  Ralf Jung authored 8 years ago
  
  c6051ad0
- define typed_read; prove type_deref and read_own_copy · f9834335
  Ralf Jung authored 8 years ago
  
  f9834335
- typed_instr and typed_body need the heap_ctx; prove assignment (based on typed_writing) · c8f39283
  Ralf Jung authored 8 years ago
  
  c8f39283
- change semantics of typed_writing to make proofs simpler · cf158914
  Ralf Jung authored 8 years ago
  
  cf158914
- move things around a little; prove first new typed-writing · 8c06d73c
  Ralf Jung authored 8 years ago
  
  8c06d73c
- show typing a let-bound instruction · a8533d30
  Ralf Jung authored 8 years ago
  
  a8533d30
Dec 20, 2016
- Robbert fixed intro patterns in proofmode :) · 977f570c
  Ralf Jung authored 8 years ago
  
  977f570c
- cleanup · 9af5ee4f
  Ralf Jung authored 8 years ago
  
  9af5ee4f
- give even zero-sized types some thread-local storage · 2e1f67ac
  Ralf Jung authored 8 years ago
  
  2e1f67ac
- prove jump to a continuation · 0f111789
  Ralf Jung authored 8 years ago
  
  0f111789
- also show wp_app for lists · 4ef23f59
  Ralf Jung authored 8 years ago
  
  4ef23f59
- prove calling a function · 889ac80b
  Ralf Jung authored 8 years ago
  
  889ac80b
- wp_app: remove commented-out tactics · 04a54e2c
  Ralf Jung authored 8 years ago
  
  04a54e2c
- show an induction principle to handle n-ary applications · a199e3f7
  Ralf Jung authored 8 years ago
  
  a199e3f7
Dec 19, 2016
- product and sum preserve Send/Sync · 02ef8176
  Ralf Jung authored 8 years ago
  
  02ef8176
- show that pointer types are Send/Sync · 6f3898c6
  Ralf Jung authored 8 years ago
  
  6f3898c6
- fn, int, bool are Send and Sync · 3e0564c7
  Ralf Jung authored 8 years ago
  
  3e0564c7
- prove declaring a continuation. it's magic. · cef7d2aa
  Ralf Jung authored 8 years ago
  
  cef7d2aa
- add Sync; get rid of Send and Copy for type contexts · 8a0cdda5
  Ralf Jung authored 8 years ago
  
  8a0cdda5
- rename mem_instructions -> mem · ce33a856
  Ralf Jung authored 8 years ago
  
  ce33a856
- prove typing a function · 40803f1d
  Ralf Jung authored 8 years ago
  
  40803f1d
- add notion of types and type contexts being Send · 00689c42
  Ralf Jung authored 8 years ago
  
  00689c42
- prove the empty list case of calling a function · ca917d76
  Ralf Jung authored 8 years ago
  
  ca917d76
- make continuation context constructor print properly · 4d689273
  Ralf Jung authored 8 years ago
  
  4d689273
- state calling and typing a function · 8be97ae8
  Ralf Jung authored 8 years ago
  
  8be97ae8
- vector-based substitution · e8b5ce29
  Ralf Jung authored 8 years ago
  
  e8b5ce29
- add notion of copyable type contexts · 845c8fa1
  Ralf Jung authored 8 years ago
  
  845c8fa1
- define typing for instructions; int and bool now no longer import any of the outdated def.s · 7c4e39bc
  Ralf Jung authored 8 years ago
  
  7c4e39bc
Dec 18, 2016
- Copy should be an implicit argument · b92c98da
  Ralf Jung authored 8 years ago
  
  b92c98da
- rename some eqtype lemmas · d3414ad2
  Ralf Jung authored 8 years ago
  
  d3414ad2
- old subtyping is not used any more, comment it out · 2fc79e0d
  Ralf Jung authored 8 years ago
  
  2fc79e0d
- splitting and merging of shared borrows · 3484f260
  Ralf Jung authored 8 years ago
  
  3484f260
- merging and splitting of unique borrows · 1b295b41
  Ralf Jung authored 8 years ago
  
  1b295b41
- split old and new definitions in typing.typing · 37085f64
  Ralf Jung authored 8 years ago
  
  37085f64
Dec 17, 2016
- try not to import uninit in own · 281d4f18
  Ralf Jung authored 8 years ago
  
  281d4f18
Dec 16, 2016
- move things around for hopefully more parallel building · 1fdaafa0
  Ralf Jung authored 8 years ago
  
  1fdaafa0
- re-prove splitting owned pointers for the new type system · 5492410f
  Ralf Jung authored 8 years ago
  
  5492410f
- locally teach solve_ndisj how to handle these inclusions · a0961de3
  Ralf Jung authored 8 years ago
  
  a0961de3
- on a newer Iris version, the solve_ndisj works somewhat better · c72bfec9
  Ralf Jung authored 8 years ago
  
  c72bfec9