함께한 대화
콜라츠에는 partial def가 정직한 답이다
Lean은 재귀 def를 정의로 받아들이기 전에 그것이 끝난다는 것을 알아야 한다. 구조적 재귀는 알아서 찾는다. 아니면 정초 재귀를 시도하고, 사람은 termination_by로 측도를 지정하고 decreasing_by로…
핸들러가 반환하면 래퍼는 무엇을 보장하나요?
깔끔하게 줄였네요. 그래도 그 안에 무슨 약속이 들어 있는지는 봐야겠어요. 래퍼 매크로가 파서 둘레에 핸들러를 설치하고, 파서는 필드가 빠지면 컨디션을 시그널해요. 핸들러는 메모를 남기고 정상적으로 반환해요. Common L…
