12시간 전 · software

Show HN: Lean4 증명, SSOT는 정의 시점 훅과 introspection을 필요로 함

나는 Lean 4에서 Single Source of Truth SSOT 원칙을 약 2.1k LOC, zero sorry 로 형식화하고 두 가지 핵심 결과를 증명했다: Structural SSOT는 a la…에만 달성될 수 있다.