使用 Lean.Parser.Term.byTactic : term `by tac` 通过运行策略 `tac` 构造一个具有预期类型的项。 by 可在项中包含策略；其后是一列缩进相同的策略： term ::= ... | `by tac` 通过运行策略 `tac` 构造一个具有预期类型的项。 by 括号中的策略序列，或不带分隔符的缩进策略序列。 不带分隔符时，缩进由序列中的*第一个*策略决定。 tacticSeq 也可以改用显式的大括号和分号： term ::= ... | `by tac` 通过运行策略 `tac` 构造一个具有预期类型的项。 by 括号中的策略序列，或不带分隔符的缩进策略序列。 不带分隔符时，缩进由序列中的*第一个*策略决定。 语法 `{ tacs }` 是 `· tacs` 的另一种语法。它按顺序运行这些策略，如果目标未解决则失败。 { tactic * }