Mario Carneiro
Mario Carneiro
```lean open foo as bar (a b c) hiding d e renaming f->g ``` Lean 4 supports the `(...)` explicits, `hiding` and `renaming` each individually, but not in conjunction, and...
In lean 3, you can use `(x y z OP e)` as a binder whenever `OP` is a binary operation, and it abbreviates the binder sequence `(x y z :...
Mathlib has a bunch of primed tactics, which either fix bugs or do things slightly differently than the unprimed tactics. We should go through the list and merge as many...
This and #2267 are two implementations of the same feature, merge only one. This modifies the desugaring for the cdot parser to apply eta-reduction to the resulting term if possible....
In the example ```lean inductive WF : Nat → Type 1 | mk (α : Type) (fn : α → Nat) (arg : α) : WF (fn arg) ``` the...
Previously, if `foo` is deprecated then the entire `simp [foo]` call would be highlighted. This causes issues for a linter I am writing which requires that the warning just cover...
> Should we have a `set_option trace.compiler.ffi_accessors` option to dump [field ordering and accessor information] for user structures? _Originally posted by @eric-wieser in https://github.com/leanprover/lean4/pull/3915#discussion_r1585705089_
More experimentation per #3046. This tries to solve the performance issue without changing the implementation, with two observations: * Most code doesn't actually care to track the size, and need...
Continuation of #3958. To ensure that lean code is able to uphold the invariant that `String`s are valid UTF-8 (which is assumed by the lean model), we have to make...
With `omega` in core, it is now more feasible to perform the necessary proofs to eliminate the `partial` from `Array.qsort`, as well as the many uses of `Array.get!` and `Array.swap!`....