doc: explain namespace indentation

Open Kha opened this issue 2 years ago • 4 comments

Oct 13 '23 11:10 Kha

I think it would be better to just remove the indentation. If indentation is not desired in actual code, why would should it be included in these examples. It only adds mental workload for anybody trying to learn Lean.

Oct 13 '23 13:10 markusschmaus

✅ Mathlib branch lean-pr-testing-2681 has successfully built against this PR. (2023-10-13 14:20:28) View Log

Oct 13 '23 14:10 leanprover-community-mathlib4-bot

I think it would be better to just remove the indentation. If indentation is not desired in actual code, why would should it be included in these examples. It only adds mental workload for anybody trying to learn Lean.

@david-christiansen Happy to leave that decision to you :)

Oct 19 '23 07:10 Kha

Note, section.md should be adjusted correspondingly. Perhaps we should merge them even?

Nov 02 '23 10:11 Kha