The first sentence of the #eval docstring in
src/Lean/Parser/Command.lean defines the command in terms of itself:
#eval e evaluates the expression e by compiling and evaluating it.
Since this docstring appears on hover in editors and on
live.lean-lang.org, it's often a newcomer's first encounter with the
command, which makes the circularity a bit unfortunate.
A small rewording would make it more informative for first-time readers,
e.g.:
#eval e compiles the expression e to executable code, runs it,
and displays the result.
The rest of the docstring (ToExpr/Repr/ToString handling, monad
adaptation, the sorry check, etc.) is fine and would be untouched.
Happy to send a PR if a change here would be welcome — and equally
happy to defer to a maintainer's preferred phrasing.
The first sentence of the
#evaldocstring insrc/Lean/Parser/Command.leandefines the command in terms of itself:Since this docstring appears on hover in editors and on
live.lean-lang.org, it's often a newcomer's first encounter with the
command, which makes the circularity a bit unfortunate.
A small rewording would make it more informative for first-time readers,
e.g.:
The rest of the docstring (ToExpr/Repr/ToString handling, monad
adaptation, the
sorrycheck, etc.) is fine and would be untouched.Happy to send a PR if a change here would be welcome — and equally
happy to defer to a maintainer's preferred phrasing.