1926.lean:6:8-6:24: warning: declaration uses `sorry`