Kyle Miller

I mentioned this to Yael already, but I had a couple documentation suggestions in #13726 along with an arguably missing lemma, but the lemma can wait for a future PR...

@robertylewis I had some documentation suggestions in #13726 (a PR targeting this branch), and there's a lemma that would be nice to have (`triangle_free_far_iff`) since the exact definition of `triangle_free_far`...

Some self-contained examples: ```lean open tactic lean lean.parser interactive interactive.types meta def tactic.interactive.trace_exact (q : parse texpr) : tactic unit := do tgt : expr ← target, e ← i_to_expr_strict...

If I understand it correctly, if a function is tagged `noncomputable` then the equation compiler will change how it compiles recursive definitions https://github.com/leanprover-community/lean/blob/master/src/library/equations_compiler/compiler.cpp#L351 All `noncomputable theory` seems to do is...

@jchoules I collected some results I had about single-vertex and single-edge subgraphs along with some of your lemmas from #16382. I'm not sure about names -- you had `vertex_singleton` and...

Thanks! bors r+

Thanks! bors r+

I had wondered about this behavior of the pretty printer before, and [this Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Forall.20vs.2E.20if-then/near/299317772) led me to check how hard it would be to make the change. If it's...

> Do you think using underscores for the variable names in non-dependent binders is a good idea? I think that would remove the downside regarding dependent types. I like this...

[(Zulip PR Reviews thread)](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/lean.23770/near/300819312)