Gabriel Ebner

> Rather than having a hard-coded handler, users can register their own code actions I think it is a good approach to make the `codeAction` extensible in this way, and...

@leodemoura I can look into this, unless you have concerns about the feature.

> I tried to create a version with a simpler type signature, namely > > ```lean > @[extern] unsafe def isSharedUnsafe : @& α → Bool > ``` This is...

That's the expected output, right? `x` is not shared, so it returns false.

Ah, this is interesting. Apparently the interpreter can only call native functions using the "boxed" wrapper. And from what I can tell, the "boxed' wrapper *always* takes owned arguments. (I'm...

> take the argument **owned** I mean this: ```lean @[extern "lean_is_shared_extern"] unsafe opaque isSharedUnsafe (a : α) : Bool ``` Note the missing `@&`. > Isn't that dangerous? No, just...

Ah yeah, you're right of course. I guess you could change the check to `rc > 2` then.

You might be interested in this discussion from another issue: https://github.com/leanprover/lean4/issues/369#issuecomment-1017837443

I think a good challenge is to get the reformatted Lean code to compile. That is, try `scripts/reformat.lean` on the whole Lean code base, try to compile it, and see...

Another fun issue related to indentation-sensitive syntax: ```lean (let x : α := a₁ b x) ``` Note that this does not compile!