In reviewing https://github.com/impermeable/bewijzen-in-de-wiskunde-lean/pull/7 I gave the feedback that "tactics" is kind of technical language, and @Michaillus rightfully pointed out we use this in the interface.
My proposal is to rename any user-facing use of "tactics" to something else.
Options:
- Phrases
- Sentences
- Steps
- Something else
@jim-portegies @jellooo038 Any opinions on this?
In reviewing https://github.com/impermeable/bewijzen-in-de-wiskunde-lean/pull/7 I gave the feedback that "tactics" is kind of technical language, and @Michaillus rightfully pointed out we use this in the interface.
My proposal is to rename any user-facing use of "tactics" to something else.
Options:
@jim-portegies @jellooo038 Any opinions on this?