Mac Malone

Following Lean style, the `size_t` definitions should not have underscores (as they are not theorems or macros). I would suggest renaming, e.g., `get_size_t_Type` to `getUSizeType` since `USize` is the Lean...

@Kha I noticed that you removed the whitespace customization. While it may be really used in the Lean core, I think it will be very useful for DSLs. Particularly, for...

@Kha > Existing token functions can simply be parameterized over the whitespace parser if desired, In my case, that would still require a separate grammar for C w/ Lean comments...

@david-christiansen The speedcenter is failing because the Lake benchmark is using this coercion in its lakefile: https://github.com/leanprover/lean4/blob/32dcc6eb895b58df3d3241a2521963e64995b621/tests/bench/inundation/lakefile.lean#L10-L12 This can be changed to `roots := #[.mkSimple test]`. **EDIT:** Applied it myself...

@digama0 > @tydeu How do you think lake should handle this? The issue is that because lean returns a nonzero error code. One other issue to consider is how partial...

@semorrison I think a change like this makes a lot of sense! `CoeFun` as it is described in the docs is designed to covert a non-function type to a function...

Code-wise, this doc needs to change to `CoeOTC` also : https://github.com/leanprover/lean4/blob/d420252dcf9f419cc33944b4a0caad730ab25a5c/src/Init/Coe.lean#L102

Coming back to this, I noticed that this doc also needs to be changed to `CoeOTC`: https://github.com/leanprover/lean4/blob/84431c2eeb3064f1220d7ede8b820055bf367072/src/Init/Coe.lean#L260

@drcicero Hello! To link to a shared library, specifying the linking flags via `moreLinkArgs` in the Lake configuration file is the currently recommended way. Alloy delegates the management of linking...

@drcicero > For example when using just `moreLinkArgs := #["-lsqlite3"]` There is mixed of news here. The good news is that is does seem to be successfully linking to a...