begin/end 블록 표기법은 lean 3 문법입니다. Lean 4에서 전술 모드를 시작하려면 by 키워드를 씁니다. 예를 들어:
example (a b c : Prop) : ((a ∨ b) → c) ↔ ((a → c) ∧ (b → c)) := by sorry
이제 공백으로 범위를 정하므로 대응하는 end는 없지만, 선택적으로 마지막에 쓰는 done는 목표가 남아 있으면 오류를 냅니다.
lean 3 경험이 많더라도 변화와 개선이 상당하므로 매뉴얼(https://lean-lang.org/lean4/doc/)이나 Theorem Proving in Lean/Functional Programming in Lean(매뉴얼의 4장과 5장)을 훑어보기를 권합니다.
end 키워드는 여전히 섹션과 네임스페이스를 닫기 때문에 여기서 end를 쓰면 그런 진단이 나옵니다.
영어에서 번역·원문 보기The begin/end block notation belongs to lean 3. To start tactic mode with Lean 4, use the keyword by, for example:
example (a b c : Prop) : ((a ∨ b) → c) ↔ ((a → c) ∧ (b → c)) := by sorry
There is no corresponding end now because white space determines the scope, although an optional final done produces an error when a goal remains open.
Even with substantial lean 3 experience, I'd suggest looking through the manual (https://lean-lang.org/lean4/doc/) and/or Theorem Proving in Lean/Functional Programming in Lean (chapters 4 and 5 of the manual), given the considerable improvements and changes.
The end keyword still closes sections and namespaces, explaining the diagnostic you see when using end here.
