All pull requests

Pull requests

• Reduce terminal returns in step

  #1397·andricicezar opened Oct 5, 2026Collaborator·3/3·

  ·

• Fix an issue with shared borrow creation

  #1394·sonmarcho opened Oct 2, 2026Member·

  ·
  1

• Model next_back for slice::Iter

  #1386·jmchapman opened Sep 30, 2026Contributor·

  ·
  1

• feat: simprocs to turn a literal scalar value into a literal Nat/Int

  #1376·abentkamp opened Sep 28, 2026Collaborator·

  ·
  1

• Lean backend: Type comparisons as Bool

  #1374·Mr-Pine opened Sep 27, 2026·

  ·
  1

• Model the TakeWhile iterator adapter

  #1373·jmchapman opened Sep 27, 2026Contributor·

  ·
  1

• Fix: crash on 64 bits variant discriminant

  #1365·CharlyCst opened Sep 25, 2026·

  ·
  1

  1

• Add missing From<bool> scalar instances

  #1361·skwh54 opened Sep 25, 2026·

  ·
  1

• Extending with separation logic

  #1352·andricicezar opened Sep 17, 2026Collaborator·2/3·

  ·
  16

• fix: look for shadowing with qualified names

  #1326·clementblaudeau opened Sep 1, 2026Collaborator·

  ·

• add an lake exe summarize command

  #1325·mpenciak opened Sep 1, 2026Collaborator·

  ·
  1

• Fix translation of iterators over arrays .

  #1314·mpenciak opened Aug 28, 2026Collaborator·

  ·

• Rename Result to RustM

  #1297·abentkamp opened Aug 25, 2026Collaborator·

  ·

• Upgrade to lean 4.33.1

  #1283·RulerOfTheQueendom opened Aug 22, 2026·

  ·

• feat: reduce Errors to only panic and undef

  #1272·abentkamp opened Aug 19, 2026Collaborator·

  ·
  8

• Trait inst notation

  #1270·mpenciak opened Aug 18, 2026Collaborator·

  ·

• Go-to-Rust-Def

  #1269·mpenciak opened Aug 18, 2026Collaborator·

  ·
  7

• Add instances so plausible (property based testing) works with Aeneas objects

  #1262·oliver-butterley opened Aug 14, 2026Collaborator·1 task·

  ·
  2

• Add div_ceil specs for the unsigned scalar types

  #1261·eKisNonos opened Aug 14, 2026·

  ·

• Support checked arithmetic binops (AddChecked/SubChecked/MulChecked)

  #1258·MantasBaksys opened Aug 13, 2026·

  ·
  1

• Add lsp info for impl_def

  #1255·oliver-butterley opened Aug 11, 2026Collaborator·

  ·
  1

  7

• Fix model of subslices for start = end case

  #1238·abentkamp opened Jul 29, 2026Collaborator·

  ·

• add api for slice/vec/array

  #1237·oliver-butterley opened Jul 28, 2026Collaborator·

  ·
  4

• add spec_refl

  #1236·oliver-butterley opened Jul 28, 2026Collaborator·

  ·
  1

• fix: replace sorrys with noncomputable opaque/axiom

  #1235·abentkamp opened Jul 27, 2026Collaborator·

  ·
  1

  1