Lean должен знать, что рекурсивный def завершается, прежде чем принять его как определение. Структурную рекурсию он находит с…
