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

Snippets Groups Projects

Jan 10, 2017
- use the fact that we can specialize lemmas below later · a7eff7e2
  Ralf Jung authored 8 years ago
  
  a7eff7e2
- Typechecking unwrap_or. · b643319a
  Jacques-Henri Jourdan authored 8 years ago
  
  b643319a
- prove writing to Cell; tune some notation · 62785d61
  Ralf Jung authored 8 years ago
  
  62785d61
- Type-checking option_as_mut. · 261c1966
  Jacques-Henri Jourdan authored 8 years ago
  
  261c1966
- typing/tests: make all the functions values as they should be · 81c01a0e
  Ralf Jung authored 8 years ago
  
  81c01a0e
- Prove that Cell<T> is a type and copy if T is copy · 97bb9b8b
  Ralf Jung authored 8 years ago
  
  97bb9b8b
- try and fail to make using ty_size_eq on \later own more convenient · 27e2cf0a
  Ralf Jung authored 8 years ago
  
  27e2cf0a
- hide the lifetime logic CMRAs behind the signature as well · deb9298d
  Ralf Jung authored 8 years ago
  
  deb9298d
Jan 09, 2017
- Trying to clarify priorities of mergeing and splitting lemmas. Clearly, this is still not optimal. · 7726a27b
  Jacques-Henri Jourdan authored 8 years ago
  
  7726a27b
- use solve_inG tactic · 477f0e9b
  Ralf Jung authored 8 years ago
  
  477f0e9b
- Simplify the proof of init_prod. · 015a5d52
  Jacques-Henri Jourdan authored 8 years ago
  
  015a5d52
- Make the pattern for [tctx_extract_hasty_here_eq] more robust. · d2b01768
  Jacques-Henri Jourdan authored 8 years ago
  
  d2b01768
- New example : init_prod. · 58e7c681
  Jacques-Henri Jourdan authored 8 years ago
  
  58e7c681
- Type unbox. · a9ab999a
  Jacques-Henri Jourdan authored 8 years ago
  
  a9ab999a
Jan 07, 2017
- Fix build : forgot a file. Also, some tweaks to simplify the proofs. · 6f46c73c
  Jacques-Henri Jourdan authored 8 years ago
  
  6f46c73c
- Type-checked second program : rebor. · d7068302
  Jacques-Henri Jourdan authored 8 years ago
  
  d7068302
Jan 06, 2017
- Define the functors for the lifetime logic · 81ab6978
  Ralf Jung authored 8 years ago
  
  81ab6978
- update Iris · ba921215
  Ralf Jung authored 8 years ago
  
  For some reason I have to fix some diverging proof scripts
  ba921215
- show that the lifetime logic can be initialized · 25f2d41c
  Ralf Jung authored 8 years ago
  
  25f2d41c
- More reformulation of typing lemmas. · 7df9982d
  Jacques-Henri Jourdan authored 8 years ago
  
  7df9982d
- Seal lifetime logic behind a signature · 8d46a3e9
  Ralf Jung authored 8 years ago
  
  Coq's module system is wholly inadequate :/
  8d46a3e9
- Expressed some instructions typing lemmas in terms of typed_body. · 4512e9a0
  Jacques-Henri Jourdan authored 8 years ago
  
  4512e9a0
- add 'Proof Using' hints to enable -quick compilation · 0e3bc878
  Ralf Jung authored 8 years ago
  
  0e3bc878
- fix build · 25a16da6
  Ralf Jung authored 8 years ago
  
  25a16da6
- turn some judgements into Iris assertions · 19eb7405
  Ralf Jung authored 8 years ago
  
  19eb7405
- Typing a function is simpler when non-recursive. · e4e4564d
  Jacques-Henri Jourdan authored 8 years ago
  
  e4e4564d
- Added a lemma for sharing without reborrowing. · 258605b5
  Jacques-Henri Jourdan authored 8 years ago
  
  258605b5
- Typechecked my first program ! · e09b9518
  Jacques-Henri Jourdan authored 8 years ago
  
  e09b9518
- WIP iApply diverges · 9d3c8aa6
  Ralf Jung authored 8 years ago
  
  9d3c8aa6
Jan 05, 2017
- Some hints were missing. · 6a821906
  Jacques-Henri Jourdan authored 8 years ago
  
  6a821906
- Tweaking. · b7505585
  Jacques-Henri Jourdan authored 8 years ago
  
  b7505585
- Automation for merging products. · a32d96ca
  Jacques-Henri Jourdan authored 8 years ago
  
  a32d96ca
- Automation for splitting products. · a34cb16b
  Jacques-Henri Jourdan authored 8 years ago
  
  a34cb16b
- Fix build. · 3ff124b7
  Jacques-Henri Jourdan authored 8 years ago
  
  3ff124b7
- Fix build by implementing th things I forgot. · 7de5f909
  Jacques-Henri Jourdan authored 8 years ago
  
  7de5f909
- Solve some todos about automation. · 04aa8db4
  Jacques-Henri Jourdan authored 8 years ago
  
  04aa8db4
Jan 04, 2017
- Make the size of uninit compute. · a7b6d7e4
  Jacques-Henri Jourdan authored 8 years ago
  
  a7b6d7e4
- Remove Closed assumptions by using the type context. · a16a3137
  Jacques-Henri Jourdan authored 8 years ago
  
  a16a3137
- prove lifetime equalizing · 261a207a
  Ralf Jung authored 8 years ago
  
  261a207a
- Writing the discriminant of a sum. · 55e3185a
  Jacques-Henri Jourdan authored 8 years ago
  
  55e3185a