lean4

lean4 copied to clipboard

refactor: simplify `Array.findIdx?` code

1

This shortens `Array.findIdx?` code, by using termination_by (and well-founded recursion) instead of a structural recursion trick, with the intent to make it more proof friendly. One motivation is that it...

michelsol

feat: `modifyM`/`modifyGetM` for `IO.Ref`

4

Adds `IO.Ref.modfyM` / `IO.Ref.modifyGetM` which are monadic variants of `IO.Ref.modify` (`ST.Prim.Ref.modify`) / `IO.Ref.modifyGet` (`ST.Prim.Ref.modifyGet`). Like them, it uses `ST.Prim.Ref.take` to atomically modify the reference via busy-waiting, but allow users to...

tydeu

feat: define `pp_using_anonymous_constructor` attribute and apply it

1

Implements a Lean 3 pretty printer feature. Structures with the `@[pp_using_anonymous_constructor_attribute]` pretty print like `⟨x, y, z⟩` rather than `{a := x, b := y, c := z}`. Adds this...

kmill

fix: handle delayed-assigned mvars in `isDefEq` safely

3

Currently, unknown fvars can be introduced during `isDefEq` when synthetic opaque metavariables are assignable and appear in a delayed assignment. Specifically, if `?m.23` is delayed-assigned to `?a`, we currently replace...

thorimur

feat: incremental elaboration of definition headers, bodies, and top-level tactic blocks

1

Implements a syntax-based approach for incremental reporting and reuse for the following intra-command elaboration steps: * finished definition (`def`/`theorem`/`abbrev`/`opaque`/`instance`/`example`) headers (binders and result type) when all syntax above is unchanged...

Kha

chore: pr-release: fix MESSAGE calculation

1

previously there was a logic bug where the check if a std tag exists would override the result of whether a mathlib tag exists (both wrote `MESSAGE` in both cases)....

nomeata

refactor: ArgsPacker

2

This introduces the `ArgsPacker` module and abstraction, to replace the exising `PackDomain`/`PackMutual` code. The motivation was that we now have more uses besides `Fix.lean` (`GuessLex` and `FunInd`), and the code...

nomeata

This PR fixes an issue where the file worker would not provide the client with semantic tokens until the file had been elaborated completely. The file worker now also tells...

mhuisi

feat: refactor of BitVec/Bitblast.lean

1

This is being overtaken by events as Henrik is working on a real bitblaster, but I would still like to sort out this file, and at some point Henrik is...

kim-em

fix: do not dllexport symbols in core static libraries

6

On Windows, we now compile all core `.o`s twice, once with and without `dllexport`, for use in the shipped dynamic and static libraries, respectively. On other platforms, we export always...

Kha