batteries

batteries copied to clipboard

`runLinter` should determine the target module by asking Lake

2

kim-em

feat: dependent array type

1

Implementation of dependent array type. [Discussion on Zulip](https://leanprover.zulipchat.com/#narrow/stream/348111-batteries/topic/RFC.3A.20.60Object.60.20and.20.60ObjectArray.60.20types/near/440896963)

fgdorais

As opposed to `def` and `abbrev`, `alias` does not open the namespaces of the declaration it is in: ``` import Batteries.Tactic.Alias def Foo.bar : Nat := 0 alias Foo.baz :=...

YaelDillies

feat: add `#help` commands

1

- [ ] Prepare Mathlib adaptation [Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/348111-batteries/topic/Upstreaming.20.23help.20command.3F/near/473358619)

fgdorais

fix: use `by rfl` instead of `rfl` to bypass new compiler bug

3

This is a workaround for a bug reported on the [zulip thread](https://leanprover.zulipchat.com/#narrow/stream/348111-batteries/topic/Large.20vector.20hangs/near/473252482)

Shreyas4991

feat: add `#check_note` command

7

on [zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Where.20to.20find.20.22notes.22) it was mentioned that there used to be an easy way to find and/or read library notes, but that this feature no longer works, presumably since lean4. This...

edegeltje

feat: add `#print opaques` command

1

WIP Co-authored-by: Mario Carneiro

fgdorais

qsort parameter name changed from "lt" to "f" since it now can be a

lyphyser

- [x] depends on: #952

kim-em

feat: the trailingWhitespace linter

4

The `trailingWhitespace` linter is a syntax linter. It emits a warning whenever a line ends with a space or a file does not end with a line break. [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/348111-batteries/topic/no.20more.20.60make.60/near/462660015)

adomani