Commits · 8464c9620e076b29c874061bce5c6f565ee9c3e1 · Lennard Gäher / Refinedrust Dev

Mar 06, 2025
- feat(na): Add simple typing rule for shared na · 8464c962
  Vincent Lafeychine authored 11 months ago
  
  8464c962
- chore(na): Remaining proofs of the simple shared lemma · 9ba1e86e
  Vincent Lafeychine authored 11 months ago
  
  9ba1e86e
- feat(na): Add simple shared lemma · 2933db88
  Vincent Lafeychine authored 1 year ago
  
  2933db88
- chore(na): Add examples + owned definition · 63bfc04f
  Vincent Lafeychine authored 1 year ago
  
  63bfc04f
- feat(na): First definition · 6aacee00
  Vincent Lafeychine authored 1 year ago
  
  6aacee00
Mar 04, 2025
- cell stuff from meeting · 341329a9
  Lennard Gäher authored 1 year ago and Vincent Lafeychine committed 1 week ago
  
  341329a9
- cell impl to play with · 40ac1a80
  Lennard Gäher authored 1 year ago and Vincent Lafeychine committed 1 week ago
  
  40ac1a80
Feb 12, 2025
- adapt docs · e83196f8
  Lennard Gäher authored 1 month ago
  
  e83196f8
- add shortcut specs also for closures · 2e378abb
  Lennard Gäher authored 1 month ago
  
  2e378abb
- fix naming issue · 86faa6d7
  Lennard Gäher authored 1 month ago
  
  86faa6d7
- allow specs without args · 7aa58674
  Lennard Gäher authored 1 month ago
  
  7aa58674
- qed time fixes · 2356b6d8
  Lennard Gäher authored 1 month ago
  
  2356b6d8
- fix existentials to allow vec rectypes again · 7c1c9c9e
  Lennard Gäher authored 1 month ago
  
  7c1c9c9e
- fix rep hook override · 6e5c85b6
  Lennard Gäher authored 1 month ago
  
  6e5c85b6
Feb 11, 2025
- fix spin · b1058e12
  Lennard Gäher authored 1 month ago
  
  b1058e12
- fixes + closure obs annotations · 2119c3b9
  Lennard Gäher authored 1 month ago
  
  2119c3b9
- first attempt at xts · ce1e1210
  Lennard Gäher authored 2 months ago
  
  ce1e1210
Feb 10, 2025
- add comment about slow qed · 78a89a55
  Lennard Gäher authored 1 month ago
  
  78a89a55
- fix function subtype sidecond · 2e93dab3
  Lennard Gäher authored 1 month ago
  
  2e93dab3
- fix · 4412000e
  Lennard Gäher authored 1 month ago
  
  4412000e
- seal ty_lfts · 1f696cf1
  Lennard Gäher authored 1 month ago
  
  1f696cf1
Feb 09, 2025
- seal ty_wf_E · 62ffc233
  Lennard Gäher authored 1 month ago
  
  62ffc233
Feb 07, 2025
- fix · fd8071bf
  Lennard Gäher authored 1 month ago
  
  fd8071bf
- try2 · 27b19ed8
  Lennard Gäher authored 1 month ago
  
  27b19ed8
Feb 05, 2025
- close lemma · 083ef14f
  Lennard Gäher authored 1 month ago
  
  083ef14f
- fix · dc96b066
  Lennard Gäher authored 1 month ago
  
  dc96b066
Feb 04, 2025
- fix ghost_drop · 4b261a58
  Lennard Gäher authored 1 month ago
  
  4b261a58
- generate rectype def · cee0e1f6
  Lennard Gäher authored 1 month ago
  
  cee0e1f6
Feb 02, 2025
- work on non-expansiveness infrastructure for enums · 17185850
  Lennard Gäher authored 1 month ago
  
  17185850
- frontend: fixes for recursive types · 5dc22dc4
  Lennard Gäher authored 1 month ago
  
  5dc22dc4
Jan 31, 2025
- revert OnceCell change · 4d9c879c
  Lennard Gäher authored 1 month ago
  
  4d9c879c
- more work on rectypes · 7388add9
  Lennard Gäher authored 1 month ago
  
  7388add9
Jan 28, 2025
- work on existentials · 56e89c6c
  Lennard Gäher authored 1 month ago
  
  56e89c6c
Jan 27, 2025
- work on lft morphisms · 154981a6
  Lennard Gäher authored 1 month ago
  
  154981a6
- mut ref contractive · bbc88713
  Lennard Gäher authored 1 month ago
  
  bbc88713
Jan 23, 2025
- change argument order for mut_ref · ac7065f0
  Lennard Gäher authored 1 month ago
  
  ac7065f0
- make progress on defining fixpoints · 29d4a7b2
  Lennard Gäher authored 1 month ago
  
  29d4a7b2
Jan 20, 2025
- change argument order of shr_ref · 8f03f300
  Lennard Gäher authored 1 month ago
  
  8f03f300
- split references.v · 864e808a
  Lennard Gäher authored 1 month ago
  
  864e808a
- add basic fixpoint type · dad3683a
  Lennard Gäher authored 1 month ago
  
  Co-authored-by: Lennard <Gäher<lennard.gaeher@ibm.com>
  dad3683a