6065.lean:12:0-12:7: warning: declaration uses `sorry`