TypeScript에서는 논리식이 Boolean 타입으로 즉시 평가되어 true 또는 false 값을 갖습니다.
Lean에서는 논리식이 Boolean으로 평가되지 않고 Prop 타입의 값으로 취급됩니다.
Prop는 값일 뿐만 아니라 타입으로도 사용되어 명제의 증명이 해당 타입의 값으로 표현됩니다.
명제의 참 여부는 증명(proof)이라는 값을 생성함으로써 보장되며, Lean 커널의 타입 검사를 통해 검증됩니다.
증명을 생성할 수 없는 명제(예: 2 + 2 = 5)는 false로 간주되어 그 타입의 값을 만들 수 없습니다.
동일한 명제의 여러 증명은 Proof Irrelevance 원칙에 따라 동등하게 취급됩니다.
Get notified when new stories are published for "heavy-ties-deny"