13.13. 证明🔗

调用策略(Lean.Parser.Term.byTactic : term`by tac` constructs a term of the expected type by running the tactic(s) `tac`. by) 的语法在 证明部分中描述。