Commits · main · Lennard Gäher / Refinedrust Dev · GitLab

Snippets Groups Projects

Mar 11, 2025
- move to frontend-generated test · cd339855
  Lennard Gäher authored 2 days ago
  
  cd339855
Mar 10, 2025
- fix todo · 30d3be04
  Lennard Gäher authored 3 days ago
  
  30d3be04
- contractiveness proofs · a686b940
  Lennard Gäher authored 3 days ago
  
  a686b940
- move instances + fix admit · 205a4255
  Lennard Gäher authored 3 days ago
  
  205a4255
Mar 09, 2025
- chore(na): Move test examples into own file · 70ecd62b
  Vincent Lafeychine authored 8 months ago
  
  70ecd62b
- feat(na): Add typeclass instances · f2dc6367
  Vincent Lafeychine authored 8 months ago
  
  f2dc6367
- feat(automation): Solve mask side condition · 257cf7e2
  Vincent Lafeychine authored 9 months ago
  
  257cf7e2
- chore(OpenedNa): Rename from Magic · de396f1b
  Vincent Lafeychine authored 9 months ago
  
  de396f1b
- feat(AliasType): Add stratify on shared case · d094230e
  Vincent Lafeychine authored 9 months ago
  
  d094230e
- fix(lithium): Extra now-unsued arguments removed · fee14b77
  Vincent Lafeychine authored 9 months ago
  
  fee14b77
- feat(na): Finish stratify proof for MagicLType · 3f0b6ccc
  Vincent Lafeychine authored 10 months ago
  
  3f0b6ccc
- chore(na): Add shrE mask · 84b2241e
  Vincent Lafeychine authored 10 months ago
  
  84b2241e
Mar 08, 2025
- workaround for lithium notation bug · 16fc9a57
  Lennard Gäher authored 10 months ago and Vincent Lafeychine committed 5 days ago
  
  16fc9a57
- generate more credits · 448f4136
  Lennard Gäher authored 10 months ago and Vincent Lafeychine committed 5 days ago
  
  448f4136
- feat(solve_ndisj): Add union mask solvers · 8e3623dd
  Vincent Lafeychine authored 10 months ago
  
  8e3623dd
- feat(FindNaOwn): Add an Option version · f617a2d8
  Vincent Lafeychine authored 10 months ago
  
  f617a2d8
- chore(type): Remove na_own from copy_shr_acc · 59723342
  Vincent Lafeychine authored 10 months ago
  
  59723342
- chore(MagicLType): Remove full type · 9215cf9a
  Vincent Lafeychine authored 10 months ago
  
  9215cf9a
- chore(na): Add fully-proved MagicType's typing rule · 75bf38a7
  Vincent Lafeychine authored 10 months ago
  
  75bf38a7
- try to fix things for thread_id change · 542d5909
  Lennard Gäher authored 10 months ago and Vincent Lafeychine committed 6 days ago
  
  542d5909
Mar 07, 2025
- chore(na_own): Remove π from unused places · 7d2631e2
  Vincent Lafeychine authored 10 months ago
  
  7d2631e2
- feat(na): Remove framing na token · 3599860b
  Vincent Lafeychine authored 10 months ago
  
  3599860b
- chore(na): Remove na_own in typed_place · cc84ffb5
  Vincent Lafeychine authored 10 months ago
  
  cc84ffb5
- chore(na): Add MagicType typing rules based on OpenedLType · 2cb024ae
  Vincent Lafeychine authored 10 months ago
  
  2cb024ae
- chore(na): Proof shared of Shadowed(Alias) · 322ae7a7
  Vincent Lafeychine authored 10 months ago
  
  322ae7a7
- feat(na): Add Shared case of AliasType + Modify Owned case of MagicType · 7b54b23c
  Vincent Lafeychine authored 10 months ago
  
  7b54b23c
- chore(ex_plain_t): Use the new MagicType definition · f34d3255
  Vincent Lafeychine authored 11 months ago
  
  f34d3255
- chore(MagicType): Transform into a &na-specific OpenedType · 271d55be
  Vincent Lafeychine authored 11 months ago
  
  271d55be
- feat(na): Use AliasLtype - move out ownership in new context item · 401c3946
  Vincent Lafeychine authored 11 months ago
  
  401c3946
- chore(ex_plain_t): Add UnsafeCell/Cell interaction example · 7f1ed0ac
  Vincent Lafeychine authored 11 months ago
  
  7f1ed0ac
Mar 06, 2025
- chore(ex_plain_t): Use ShadowedType + OpenedType instead of MagicType · 20890783
  Vincent Lafeychine authored 11 months ago
  
  20890783
- chore(MagicType): Mask is no longer passed through · 70336d45
  Vincent Lafeychine authored 11 months ago
  
  70336d45
- chore(MagicType): core is no longer recursive · 72bb73ea
  Vincent Lafeychine authored 11 months ago
  
  72bb73ea
- chore(na): Cpre/Cpost takes rt_cur instead of rt_full · e0592720
  Vincent Lafeychine authored 11 months ago
  
  e0592720
- chore(na): Add MagicLTy(pe) + na token pass through · 940418f4
  Vincent Lafeychine authored 11 months ago
  
  940418f4
- chore(na): Complete ty_share sidecondition · 0ccdca22
  Vincent Lafeychine authored 11 months ago
  
  0ccdca22
- feat(na): na_inv_P not Timeless and Persistant anymore · ef1a5afd
  Vincent Lafeychine authored 11 months ago
  
  ef1a5afd
- 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 11 months ago
  
  2933db88