증명, 명제 그리고 명제들의 유형

λx.x를 린에서는 λ (x : p) => xfun (x : p) ↦ x와 같이 나타낸다는 점도 제가 설명할 걸 그랬네요. 저는 오히려 λx.x 꼴의 식이 낯설어요. 아마 린 핵심 개발진은 수학자들이 선호할 만한 표기법을 고른 듯해요. 어쨌든 식 fun (x : p) ↦ x는 메타언어 문장이 아닐 거예요. 이게 그렇다면 식 λx.x도 메타언어 문장입니다.

예전에 제가 쓴 글 '증명 보조기와 유형론 알아보기'를 인용할게요.