lean4

lean4 copied to clipboard

feat: enforce indentation of command contents

5

Only affects parts using `colGt/Ge`, e.g. arguments to functions See test case for motivation

Kha

feat: bundle std4

1

Let's see if anything breaks

Kha

perf: rewrite UnusedVariables lint

23

This is a rewrite of the `UnusedVariables` lint to inline and simplify many of the dependent functions to try to improve the performance of this lint, which quite often shows...

digama0

fix: make lean4 build on FreeBSD

2

Upstreaming patches from the FreeBSD port. The port compiles successfully on FreeBSD and all but 6 tests pass.

yurivict

feat: lake: `require` overhaul

3

This PR contains major changes to `require` DSL, the Lake manifest format, types of dependencies, and the how packages and targets are named. These changes overlap in significant ways, hence...

tydeu

refactor: lake: API cleanup / mark some defs `private`

3

It has long been requested to better clarify what parts of Lake API are public and which parts are internal implementation details. This change is a small step towards that...

tydeu

feat: profile instructions on Linux

6

Kha

feat: manage nested inductive types in `deriving`

2

- Adds support for handling nested inductive types in derive handlers - Removes `usePartial`, which was used to generate partial definitions for some derive handlers, as it is no longer...

arthur-adjedj

fix: reduce let-bodies correctly in `StructInst`

1

Closes #3146 Reduction doesn't trigger correctly on the bodies of `let`-expressions in `StructInst`, leading some meta-variables to linger in the terms of some fields. Because of this, default fields may...

arthur-adjedj

feat: add `simp` configuration option `Simp.Config.instances`

5

Depends on #3124 Mathlib adaptation PR is at https://github.com/leanprover-community/mathlib4/pull/9572

leodemoura