1842.lean:7:8-7:23: warning: declaration uses `sorry`