4761.lean:7:18-7:27: warning: declaration uses `sorry`