4861.lean:2:8-2:11: warning: declaration uses `sorry`