988.lean:1:0-1:8: warning: declaration uses `sorry`
988.lean:6:8-6:20: warning: declaration uses `sorry`