602.lean:26:9-26:22: warning: declaration uses `sorry`