lean4

lean4 copied to clipboard

feat: upstream `congr!` from Mathlib

4

This is a preliminary step to upstreaming `convert`. We should later think about combining this with the standard `congr`. There is still a builtin problem here, that you can not...

kim-em

refactor: clean up public API around `Array.eraseIdx`

1

- Removes the public definitions `Array.eraseIdxAux` and `Array.eraseIdxSzAux` which were implementation details. - Motivation: `Array.eraseIdxAux` and `Array.eraseIdxSzAux` were clearly not intended to remain public, but simply making them private would...

timotree3

chore: fix namespaces in recently upstreamed tactics

1

kim-em

feat: snapshot trees and language processors

8

This is the foundation for work on making processing in the language server both more fine-grained (incremental tactics) as well as parallel. Includes: - #2959 - #3013 TODOs before merging:...

Kha

feat: lake: add `lake dump-config` command

18

This adds a mechanism to dump most of lake's workspace configuration state (everything except the functions, more or less) to standard out in JSON format. This is roughly equivalent to...

digama0

feat: FFI thread initialization

4

* #2490 * [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Expose.20thread.20management.20routines.20to.20FFI.3F/near/387373357) This exposes the following functions to FFI: ```c void lean_finalize_runtime_module(); void lean_finalize(); void lean_thread_initialize(); void lean_thread_finalize(); bool lean_in_thread_finalization(); void lean_reset_thread_local(); void lean_register_thread_finalizer(void (*fn)(void *), void...

digama0

feat: include `ppLine` in `many(1)Indent`

6

I noticed `many1Ident` did not pretty print lines during [this](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Fun.20macro.20-.20bulleted.20argument.20lists/near/384908572) Zulip thread. Including `ppLine` within `manyIdent` will help end users get better pretty printer output without needing initmate knowledge of...

tydeu

feat: add namespace utility function

8

It was pointed out in [std4#184](https://github.com/leanprover/std4/pull/184) that this function is frequently reimplemented and that it may find a better home here.

fgdorais

Sort messages by position when printing

4

As exhibited in #2276 but already encountered many times before I believe, so it is high time to make the message ordering more deterministic. Unfortunately there is some perhaps unwanted...

Kha

rfc: allow universe unification to solve `max u v =?= max u ?v`

6

See issue description at #2297.

kim-em