Commits · 7388add9e5d59569910c8e04a44f3be0abd3cb5a · Lennard Gäher / Refinedrust Dev · GitLab

Snippets Groups Projects

Jan 31, 2025
- more work on rectypes · 7388add9
  Lennard Gäher authored 1 month ago
  
  Verified
  
  7388add9
Jan 28, 2025
- work on existentials · 56e89c6c
  Lennard Gäher authored 1 month ago
  
  Verified
  
  56e89c6c
Jan 27, 2025
- work on lft morphisms · 154981a6
  Lennard Gäher authored 1 month ago
  
  Verified
  
  154981a6
- mut ref contractive · bbc88713
  Lennard Gäher authored 1 month ago
  
  Verified
  
  bbc88713
Jan 23, 2025
- change argument order for mut_ref · ac7065f0
  Lennard Gäher authored 1 month ago
  
  Verified
  
  ac7065f0
- make progress on defining fixpoints · 29d4a7b2
  Lennard Gäher authored 1 month ago
  
  Verified
  
  29d4a7b2
Jan 20, 2025
- change argument order of shr_ref · 8f03f300
  Lennard Gäher authored 1 month ago
  
  Verified
  
  8f03f300
- split references.v · 864e808a
  Lennard Gäher authored 1 month ago
  
  Verified
  
  864e808a
- add basic fixpoint type · dad3683a
  Lennard Gäher authored 1 month ago
  
  Co-authored-by: Lennard <Gäher<lennard.gaeher@ibm.com>
  Verified
  
  dad3683a
- port type_dist from rustbelt · 2b2e76dc
  Lennard Gäher authored 1 month ago
  
  Co-authored-by: Lennard Gäher <lennard.gaeher@ibm.com>
  Verified
  
  2b2e76dc
- fix ci · ddab7481
  Lennard Gäher authored 2 months ago
  
  Verified
  
  ddab7481
- improve solvers · ea55206b
  Lennard Gäher authored 2 months ago
  
  Verified
  
  ea55206b
- improve lft_incl solver · e9ee15da
  Lennard Gäher authored 2 months ago
  
  Verified
  
  e9ee15da
- remove sidecondition proof that now gets solved automatically · 673ad84e
  Lennard Gäher authored 2 months ago
  
  Verified
  
  673ad84e
- improve lft_alive solver · c9db3880
  Lennard Gäher authored 2 months ago
  
  Verified
  
  c9db3880
- make sure that local lifetimes are always constrained · 80ec77c9
  Lennard Gäher authored 2 months ago
  
  Verified
  
  80ec77c9
- improve lifetime inclusion solver to backtrack on external inclusions · 44402880
  Lennard Gäher authored 2 months ago
  
  Verified
  
  44402880
- Handle trait attributes and associated type escapes in more places · 91abe9d5
  Lennard Gäher authored 2 months ago
  
  Verified
  
  91abe9d5
- make process_coq_literal a method · 8add0d16
  Lennard Gäher authored 2 months ago
  
  Verified
  
  8add0d16
Jan 03, 2025
- remove unused imports · c2dd80f7
  Lennard Gäher authored 2 months ago
  
  Verified
  
  c2dd80f7
- split up function_body · 3aca54f4
  Lennard Gäher authored 2 months ago
  
  Verified
  
  3aca54f4
- move region management for calls and composites · 8a2d7a76
  Lennard Gäher authored 2 months ago
  
  Verified
  
  8a2d7a76
- refactor init and assignment constraints · e1708622
  Lennard Gäher authored 2 months ago
  
  Verified
  
  e1708622
- fix fmt · 8b6a5bff
  Lennard Gäher authored 2 months ago
  
  Verified
  
  8b6a5bff
Jan 02, 2025
- partial refactor of function_body · f5e500cb
  Lennard Gäher authored 2 months ago
  
  Verified
  
  f5e500cb
- remove unused imports · 3192900b
  Lennard Gäher authored 2 months ago
  
  Verified
  
  3192900b
- clean up utils · 766cae6c
  Lennard Gäher authored 2 months ago
  
  Verified
  
  766cae6c
- refactor shims · a7cbdd14
  Lennard Gäher authored 2 months ago
  
  Verified
  
  a7cbdd14
- refactor traits · 7f55bf30
  Lennard Gäher authored 2 months ago
  
  Verified
  
  7f55bf30
- fix some unused imports · a9391f57
  Lennard Gäher authored 2 months ago
  
  Verified
  
  a9391f57
- refactor type translator · 547bb618
  Lennard Gäher authored 2 months ago
  
  Verified
  
  547bb618
Dec 30, 2024
- Refactor handling of trait requirements · caf51252
  Lennard Gäher authored 2 months ago
  
  Co-authored-by: Lennard Gäher <l.gaeher@posteo.de>
  caf51252
Dec 17, 2024
- chore(coq): Add missing documentation · ab0a69d9
  Vincent Lafeychine authored 3 months ago
  
  Verified
  
  ab0a69d9
Nov 02, 2024
- feat(coq::radium): Add binders · b7125100
  Vincent Lafeychine authored 4 months ago
  
  Verified
  
  b7125100
- feat(coq::radium): Sunset old representation · 4cf4b624
  Vincent Lafeychine authored 5 months ago
  
  Verified
  
  4cf4b624
Nov 01, 2024
- chore(radium::coq): Create subcategory command · 2f479fcc
  Vincent Lafeychine authored 5 months ago
  
  Verified
  
  2f479fcc
- feat(coq::radium): Replace module crate · 8c75695a
  Vincent Lafeychine authored 5 months ago
  
  Verified
  
  8c75695a
- Use specific version of Coq (8.20) for documentation · 5acf32f5
  Vincent Lafeychine authored 5 months ago
  
  Verified
  
  5acf32f5
- chore(fix): Remove unused argument · 1a545ad5
  Vincent Lafeychine authored 5 months ago
  
  Verified
  
  1a545ad5
- feat: Add 'Hello world' example · 6bd791d7
  Vincent Lafeychine authored 7 months ago
  
  Verified
  
  6bd791d7