search

leanprover-community / lean4-metaprogramming-book

https://leanprover-community.github.io/lean4-metaprogramming-book/
Apache License 2.0
204 stars 47 forks source link

chore: switch main/03_expressions.lean to semantic linebreaks #110

Closed jcommelin closed 10 months ago

jcommelin commented 10 months ago

@Julian I think I've internalized a version of semantic line-breaks that aims for <100 chars per line. So I tend to linebreak sentences into clauses when they get too long. The benefit is that you can have the info view open on a smaller screen, and everything still fits. But maybe we just want one line per sentence, and people can word-wrap if their screen is too small...

Julian commented 10 months ago

Got it, yeah I tend to go for the latter ("it's prose now, so use word wrap if you need to") but you're right, it's definitely not the only way, so perhaps never mind my comments!

Julian commented 10 months ago

In light of the above by the way, I have no personal issues with this change, so consider it a LGTM from me if you want to merge.