Gabriel Ebner

This is getting more and more interesting: ```lean #eval tactic.is_def_eq `(0 : ℕ) `(0 : additive ℕ) -- succeeds!?! ```

Ping me please once there is something reviewable here.

Does this actually help us with mathlib CI? Does this produce too much output for the CI log? Should it rather print progress messages as JSON, so that we can...

> Seems `like : ` will be chopped off from quoted names? This is a bug in the text export parser of `leanchecker`.

I believe `set_of` is the only reason some of the `set` definition is still in core (see https://github.com/leanprover-community/lean/pull/675#issuecomment-1024411237). There's also a test that checks whether every definition referenced from the...

I don't have a strong opinion one way or the other.

IIRC it was intentional that the type parameter of list and option is in Type instead of Sort, as this simplifies type inference. Have you tried compiling mathlib with this...

You need to make a tag for the CI to upload a release. Please make the tag on your own fork.

There are two issues here: 1. The expression that is stored is not the equations, but the pre-expression of the definition (even if this is not an equation). Nothing is...

> If this is our goal, are the elaborated equations the ones we need? Yes, I'd strongly suggest that.