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