1025.lean:18:10-18:19: warning: declaration uses `sorry`