338.lean:7:4-7:7: warning: declaration uses `sorry`