nightly-2025-01-28

Changes since nightly-2025-01-27:

Full commit log

• 20c6165 feat: add grind? (#6810)
• 104b351 feat: add Fin.ofNat'_zero (#6806)
• d8fcfea feat: add LawfulMonad helper simp lemmas (#6805)
• d0b947b chore: add @[simp] to Option.not_mem_none (#6804)
• 5f0fea6 refactor: lake: deprecate -U (#6798)
• 3e54597 feat: lake query (#6323)
• eb1c9b9 chore: two BitVec lemmas that help simp confluence (#6807)
• 4d66e7b feat: add List.modifyHead_dropLast (#6803)
• f866048 feat: Option.elim_pmap, improving simp confluence (#6802)
• 64766f8 fix: offset constraint propagation in grind (#6801)
• f64bce6 fix: auto-completion performance regression (#6794)
• 0160aa1 test: identifier completion benchmark (#6796)
• 3418d6d fix: more robust equational theorems generation for partial_fixpoint (#6790)
• 3aea0fd feat: add comparison lemmas to bv_normalize (#6788)
• 4ca98dc doc: typos in partial_fixpoint related docstrings (#6787)
• 55b0bed doc: standard library vision and call for contributions (#6762)
• d86a408 feat: bv_decide can reason about equality of structures (#6740)