4673.lean:10:0-10:7: warning: declaration uses `sorry`