Sebastian Ullrich
Sebastian Ullrich
Yes, if you add `set_option pp.all true`, the context is ``` h₁ : @Eq.{1} Nat (@f.z.{0, u_1} Nat x) (@OfNat.ofNat.{0} Nat (nat_lit 0) (instOfNatNat (nat_lit 0))) w : Nat h₂...
/cc @kmill - you might be interested in this let/have difference (I didn't take a look further than Paul)
What does this mean in file size? Can you please document the code?
I can't accept this if it just throws away parts of the regex match. But for local toolchains, even the version match doesn't make much sense. How about changing the...
Oof. I'd accept a pull request but this is really quite out there...
Would this be covered by "allow lean-toolchain to directly point to a toolchain path"?