Gabriel Ebner

I think the syntax error is a red herring here. Minimized: ```lean partial def swipc (_ : Unit) : Nat × Nat := let (a, b) := swipc () (a,...

From what I can tell, the issues are all in the part of the compiler which is already written in Lean.

> Right, given that we would get the same code inline anyway if we wrote either `$x:ident` or an actual ident, do we expect this to yield significant savings? It...

One option that I just pitched to Leo was to make the `toOne` and `toMul` arguments in the `MulOneClass.mk` constructor explicit: ```lean {M : Type u_1} → (toOne : One...

And make mathlib prelude-fre

I see what you mean. The inaccessible (that's how they're called) hypothesis `‹Pairwise R l ∧ Pairwise S l›` is a leftover from pattern matching AFAICT. So it should be...

Pending discussion on Zulip: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/append.20and.20concat/near/299602232

Please title the PR `fix(util/memory): support freebsd` Otherwise LGTM.

I can't reproduce this issue. The live version on the website takes a couple of seconds to load (no matter the file), but after that your example is instantaneous.

It takes around 350ms.