Simon Hudon
It would be good to know what `x_type` is in ```cpp lean_assert(is_inductive_app(x_type)); ```
That sounds like a nice improvement. And it would also make clearer when `dismiss_review` occurs
Thanks for the fast response! Before even getting to configure the pdflatex command, I've been struggling with a few things. I record them here as much to show sign of...
That's exactly right. I'm sure it can be generalized but I really don't know where I'd begin. I propose we start with this particular case and generalize when that becomes...
@b-mehta I'd like to know more about using completeness instead of binary products and terminal objects. How do you state completeness?
@b-mehta Who should we ask to look at how we're using the concrete category API?
Actually, you can create the PR at https://github.com/cipher1024/lean-depot/blob/master/pkgs/lean-homotopy-theory.toml
Also related: @CohenCyril spent a couple of intense weeks on the problem ([his repo](https://github.com/CohenCyril/mathlib/tree/param)). It is not an easy problem and we'll have to be patient.
It was mentioned in the conversation earlier. I think the consensus was that this machinery is too ad hoc and not very extendible. I don't personally have experience with it...
How big is `tactic.localized` and how much does it depend on? This is a feature I would really love to have access to everywhere. > setup_tactic_parser opens namespaces, which open_locale...