batteries

batteries copied to clipboard

feat: the `hint` tactic

3

Note this includes the parallelisation upgrade that is still being reviewed at Mathlib as https://github.com/leanprover-community/mathlib4/pull/8435, but Leo is keen to get this into Std so I'm opening this already. Depends...

kim-em

feat: allow solve_by_elim to use projections of hypotheses

5

This powers up `solve_by_elim` by allowing it to use projections of hypotheses. It does so by saturating the context with let-bindings for projections (recursively). For interactive use of `solve_by_elim`, this...

kim-em

Add docker / gitpod integrations

4

Mathlib has `.docker` and `.devcontainer` folders that (for one thing) make it easy to quickly load in to a fresh install of lean + mathlib (eg with gitpod.io). I think...

alexjbest

feat: backport `Function.Injective` etc from Mathlib

8

Also move `Std.Logic` to `Std.Logic.Basic`.

urkud

feat: some lemmas about variations List.get and List.getLast, fix duplicate lemma

2

javra

feat: migrate List lemmas from mathlib

14

Integrates a few of Mathlib's lemmas over `List`s. Some proofs have been slightly simplified

AdrienChampion

False positive from the unusedHavesSuffices linter

5

``` import Std /---/ def npowRec {M : Type} [Mul M] (one : M) : Nat → M → M | 0, _ => one | n + 1, a...

kim-em

feat: lift StateM to StateT

2

I feel like this might already exist somewhere, but with a not too old Std/Mathlib imported it does not exist yet.

JamesGallicchio

kim-em

this goes along https://github.com/leanprover/lean4/pull/2577

nomeata