Mario Carneiro

This seems closely related to coherence checks: coherence means something like `Implemented T -> Implemented U -> T = U` while copy/drop has the form `Implemented T -> Implemented U...

Using a different word than "provenance" is not a good idea. This is a term-of-art: the fact that it does not have a common use in english is a strength...

60% joking: `recover_provenance_by_magic()`. (I like that this will make people *really* look askance at any uses of the function in code review.)

I also ran into this issue. I am translating between two formats that only need to refer to the image without loading it (the input and output both only need...

Lean 3 is EOL, so this issue is not likely to be addressed for a possibly very long time.

My lean path is a bit cluttered... I put the test directory at `lean\library\test` for convenience. $ lean -p { "is_user_leanpkg_path": false, "leanpkg_path_file": "C:\\Users\\Mario\\lean\\library\\leanpkg.path", "path": [ "C:\\Users\\Mario\\lean\\library", "C:\\Users\\Mario\\lean\\lib\\dev", "C:\\Users\\Mario\\lean\\leanpkg", "C:\\Users\\Mario\\lean\\lib\\dev\\_target\\deps\\super\\src",...

That seems exceedingly unlikely; I can't find any other `a.lean` files in the `lean` directory, which is as it should be because that's a terrible name.

If you have "baggage restrictions", another viable approach is to pluck individual theorems from mathlib and add them to your project. At least in this early section there will be...

The workaround (if you can't change the names) is to refer to `_root_.add1.succ` instead of `add1.succ`.

It is a special namespace which represents the root of the namespace hierarchy. It's like the forward slash prefix in linux-style paths. Any definition at `x.y.z` can also be accessed...