Skip to content

nightly-2024-12-03

Pre-release
Pre-release
Compare
Choose a tag to compare
@leodemoura leodemoura released this 03 Dec 08:39
· 1 commit to main since this release

Changes since nightly-2024-12-02:

Full commit log

  • cb600ed chore: restore broken proofs
  • 57d83c8 feat: add simp configuration to norm_cast macros
  • ce27d49 chore: update stage0
  • 8a7889d chore: temporarily sorry broken proofs
  • 6934029 chore: add simp configuration to norm_cast syntax
  • 222abdd feat: simprocs for other Fin operations (#6295)
  • 490be92 chore: specialize fold loops (#6293)
  • cda6d5c chore: upstream List.length_flatMap (#6294)
  • 9044043 chore: robustify for byAsSorry (#6287)
  • f6bc6b2 fix: lake: properly prepend job log in ensureJob (#6291)
  • d9d54c1 chore: lake: use & check prelude (#6289)
  • b2336fd perf: speed up bv_decide reflection using Lean.RArray (#6288)
  • f156f22 feat: lake: build without leanc (#6176)
  • 3c348d4 chore: CI: bump dawidd6/action-download-artifact from 6 to 7 (#6274)
  • 0b8f50f feat: async linting (#4460)
  • 0d89f01 perf: bv_decide uses rfl in reflection if possible (#6286)
  • e157fcb chore: missing Array/Vector injectivity lemmas (#6284)
  • 95dbac2 chore: shake Std.Time (#6283)
  • be63c82 chore: CI: bump dcarbone/install-jq-action from 2.1.0 to 3.0.1 (#6275)
  • 6fcf35e chore: script/mathlib-bench (#6280)
  • b3e0c9c fix: use sensible notion of indentation in structure instance field completion (#6279)