Expr 트리
Lean 내부에서 표현식을 계층적 노드 구조로 표현한 자료구조로서 식별자, 응용(application), 람다, 타입 정보 등이 구조적으로 보존되어 모델에 더 직접적이고 의미론적 입력을 제공할 수 있다.