策略包含在使用 Lean.Parser.Term.byTactic : term`by tac` constructs a term of the expected type by running the tactic(s) `tac`. by 的术语中，后跟策略的序列，其中每个序列具有相同的缩进：

term ::= ...
    | `by tac` constructs a term of the expected type by running the tactic(s) `tac`. by
      A sequence of tactics in brackets, or a delimiter-free indented sequence of tactics.
Delimiter-free indentation is determined by the *first* tactic of the sequence. tacticSeq

或者，可以使用明确的大括号和分号：

term ::= ...
    | `by tac` constructs a term of the expected type by running the tactic(s) `tac`. by A sequence of tactics in brackets, or a delimiter-free indented sequence of tactics.
Delimiter-free indentation is determined by the *first* tactic of the sequence. The syntax `{ tacs }` is an alternative syntax for `· tacs`.
It runs the tactics in sequence, and fails if the goal is not solved. { tactic* }