lean4

lean4 copied to clipboard

Elaboration failure with let mut whose RHS is a do notation

1

Consider the MWE: ```lean def fails : MetaM Unit := do let mut val : Bool ← do pure true -- unknown identifier val val := Bool.not val -- FAILS!...

bollu

feat: BitVec lemmas for smtUDiv, smtSDiv when denominator is zero

1

This is a follow-up to https://github.com/leanprover/lean4/pull/5609, where we add lemmas characterizing `smtUDiv` and `smtSDiv`'s behavior when the denominator is zero. We build some `slt` theory, connecting it to `msb` for...

bollu

TwoFX

feat: Upstream `MPL.SPred.*` from `mpl`

3

This PR adds a logic of stateful predicates SPred to Std.Do in order to support reasoning about monadic programs. It comes with a dedicated proof mode the tactics of which...

sgraf812

chore: Grove: high-level sections

1

TwoFX

The branch on which I try migrating the old ranges to the new ones.

datokrat

chore: test integrated Mathlib CI

1

kim-em

refactor: migrate all usages of old slice notation

7

This PR replaces all usages of `[:]` slice notation in `src` with the new `[...]` notation.

datokrat

feat: introduce slices

3

This PR introduces polymorphic slices in their most basic form. They come with a notation similar to the new range notation. `Subarray` is now also a slice and can produce...

datokrat

feat: improve projection and field-notation errors

1

This PR improves the error messages produced by invalid projections and field notation. It also adds a hint to the "function expected" error message noting the argument to which the...

jrr6