elaboration

Lean에서 표면 문법에 포함된 암시적 인수와 매크로 등이 구체적인 표현식으로 변환되는 과정으로, 소스 텍스트에 남지 않는 의미적 정보를 생성하며 이 정보를 이용하면 모델 입력에서 잡음을 줄일 수 있다.