batteries

batteries copied to clipboard

feat: add type classes for decidable < and <= relations

9

This means that instead of writing ``` def f [inst : LT α] [DecidableRel (@LT.lt α inst)] (args ...) := ... ``` users can write ``` def f [DecidableLT α]...

david-christiansen

feat: `trySetOptions` / `tryEraseAttrs` command elab helpers

9

Helpers which I wrote for @hrmacbeth to use in her Mechanics of Proof [package](https://github.com/hrmacbeth/math2001/tree/main) to help with initializing options and attributes for a teaching environment. She suggested I PR these...

tydeu

feat: run `List (MetaM x)` asynchronously, returning an `MLList MetaM x` in the order they return.

2

Depends on: * [x] https://github.com/leanprover/std4/pull/398 * [x] https://github.com/leanprover/std4/pull/397 Prerequisite for the `hint` tactic.

kim-em

chore: upstream spread syntax `__ :=`

2

kim-em

feat: make `by_cases` remember current case tag

3

astrainfinita

Fixed width signed integer datatypes.

2

Lean should provide `Int8`, `Int16`, `Int32` and `Int64` to complement `UInt8`, `UInt16`, `UInt32`, and `UInt64`. Ideally the definitions should be in core and the compiler extended to generate efficient code...

joehendrix

WIP: Roadmap document for standard library

3

This is a draft document that describes desired features in the standard library. I thought I'd submit it as a PR to the repo itself for now for feedback, but...

joehendrix

This doesn't need review for now. This is a statement of "Cooper resolution" as used in Jovanović and de Moura's "Cutting to the chase". This may eventually end up in...

kim-em

feat: let_projs tactic, recursively adding projections of hypotheses

4

`let_projs` adds let bindings for all projections of local hypotheses, recursively. It's probably rarely useful interactively, but may be useful as a preprocessing step for tactics such as `solve_by_elim`.

kim-em

chore: 'lemma' command elaborates as 'theorem' but gives warning + codeaction to use 'theorem' instead

2

jcommelin