6.13. 証明（Proofs）

タクティクを呼び出す構文（ Lean.Parser.Term.byTactic : term`by tac` constructs a term of the expected type by running the tactic(s) `tac`. by ）は 証明の節 で説明されています。