Lean은 재귀 def를 정의로 받아들이기 전에 그것이 끝난다는 것을 알아야 한다. 구조적 재귀는 알아서 찾는다. 아니면 정초 재귀를 시도하고, 사람은 termination_by로 측도를 지정하고 decreasing_by로…
