2265.lean:2:8-2:15: warning: declaration uses `sorry`