lean4

lean4 copied to clipboard

Make token parser customizable

10

In theory, users can implement arbitrary lexical grammars as the built-in token parser is merely another combinator whose use can be avoided; in practice, avoiding it also means forgoing the...

Kha

feat: `opaque_repr` attribute to suppress "trivial structure" opt

1

This adds an attribute `@[opaque_repr]` which is used by both the old and new compilers to suppress the "trivial structure" optimization (which deletes `mk` and `proj` applications for newtype structures),...

digama0

fix: respect type reducibility when generating injectivity lemmas

2

The relevant test case is: ```lean def WrappedNat (_n : Nat) := Nat structure WithWrapped : Type := (n : Nat) (m : WrappedNat n) #check WithWrapped.mk.injEq #print WithWrapped.noConfusionType ```...

eric-wieser

Alternative version of #2263 . This modifies the desugaring for the cdot parser to apply eta-reduction to the resulting term if possible. So `(· + ·)` elaborates to `HAdd.hAdd` instead...

digama0

fix: resolve `_root_` in `macro`, `syntax`, `elab`

9

This is not just a convenience feature: Because `_root_` is resolved in `def`, if we do not also resolve it in `macro` there will be a mismatch between the syntax...

digama0

There was an ABI mismatch between the storage of `@[init]` declarations and the load in the interpreter, leading to garbage results. Discussed on [Zulip](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.60lake.20exe.60.20interpreted.20mode.3F/near/361224125).

digama0

Mathlib's `library_search` is frequently picking up constants named `proof_1`, preventing it from finding more appropriate lemmas. I opened a PR there to work around the problem (https://github.com/leanprover-community/mathlib4/pull/2349), but it risks...

dwrensha

This PR normalizes usage of `binderIdent` vs `ident` across the lean grammar. To construct this PR I reviewed every occurrence of `ident` to determine whether (1) it is introducing a...

digama0

fix: #include <mutex> in mutex.cpp

2

succeeds #2091 Before this patch `unique_lock` refers to `lean::unique_lock` under certain conditions ( -DLEAN_MULTI_THREAD=OFF).

iacore

fix: LLVM backend: detect size_t from target triple

13

I added the binding API to get pointer size from target. I hope I got the lifetime right. A lot of plumbing need to be done in Lean @bollu

iacore